:: by Miros{\l}aw Jan Paszek

::

:: Received May 23, 1995

:: Copyright (c) 1995-2021 Association of Mizar Users

definition

let U0 be Universal_Algebra;

ex b_{1} being set st

for U1 being set st U1 in b_{1} holds

U1 is SubAlgebra of U0

end;
mode SubAlgebra-Family of U0 -> set means :Def1: :: UNIALG_3:def 1

for U1 being set st U1 in it holds

U1 is SubAlgebra of U0;

existence for U1 being set st U1 in it holds

U1 is SubAlgebra of U0;

ex b

for U1 being set st U1 in b

U1 is SubAlgebra of U0

proof end;

:: deftheorem Def1 defines SubAlgebra-Family UNIALG_3:def 1 :

for U0 being Universal_Algebra

for b_{2} being set holds

( b_{2} is SubAlgebra-Family of U0 iff for U1 being set st U1 in b_{2} holds

U1 is SubAlgebra of U0 );

for U0 being Universal_Algebra

for b

( b

U1 is SubAlgebra of U0 );

registration

let U0 be Universal_Algebra;

existence

not for b_{1} being SubAlgebra-Family of U0 holds b_{1} is empty

end;
existence

not for b

proof end;

definition

let U0 be Universal_Algebra;

:: original: Sub

redefine func Sub U0 -> non empty SubAlgebra-Family of U0;

coherence

Sub U0 is non empty SubAlgebra-Family of U0

:: original: Element

redefine mode Element of U00 -> SubAlgebra of U0;

coherence

for b_{1} being Element of U00 holds b_{1} is SubAlgebra of U0
by Def1;

end;
:: original: Sub

redefine func Sub U0 -> non empty SubAlgebra-Family of U0;

coherence

Sub U0 is non empty SubAlgebra-Family of U0

proof end;

let U00 be non empty SubAlgebra-Family of U0;:: original: Element

redefine mode Element of U00 -> SubAlgebra of U0;

coherence

for b

definition

let U0 be Universal_Algebra;

let u be Element of Sub U0;

ex b_{1} being Subset of U0 ex U1 being SubAlgebra of U0 st

( u = U1 & b_{1} = the carrier of U1 )

for b_{1}, b_{2} being Subset of U0 st ex U1 being SubAlgebra of U0 st

( u = U1 & b_{1} = the carrier of U1 ) & ex U1 being SubAlgebra of U0 st

( u = U1 & b_{2} = the carrier of U1 ) holds

b_{1} = b_{2}
;

end;
let u be Element of Sub U0;

func carr u -> Subset of U0 means :Def2: :: UNIALG_3:def 2

ex U1 being SubAlgebra of U0 st

( u = U1 & it = the carrier of U1 );

existence ex U1 being SubAlgebra of U0 st

( u = U1 & it = the carrier of U1 );

ex b

( u = U1 & b

proof end;

uniqueness for b

( u = U1 & b

( u = U1 & b

b

:: deftheorem Def2 defines carr UNIALG_3:def 2 :

for U0 being Universal_Algebra

for u being Element of Sub U0

for b_{3} being Subset of U0 holds

( b_{3} = carr u iff ex U1 being SubAlgebra of U0 st

( u = U1 & b_{3} = the carrier of U1 ) );

for U0 being Universal_Algebra

for u being Element of Sub U0

for b

( b

( u = U1 & b

definition

let U0 be Universal_Algebra;

ex b_{1} being Function of (Sub U0),(bool the carrier of U0) st

for u being Element of Sub U0 holds b_{1} . u = carr u

for b_{1}, b_{2} being Function of (Sub U0),(bool the carrier of U0) st ( for u being Element of Sub U0 holds b_{1} . u = carr u ) & ( for u being Element of Sub U0 holds b_{2} . u = carr u ) holds

b_{1} = b_{2}

end;
func Carr U0 -> Function of (Sub U0),(bool the carrier of U0) means :Def3: :: UNIALG_3:def 3

for u being Element of Sub U0 holds it . u = carr u;

existence for u being Element of Sub U0 holds it . u = carr u;

ex b

for u being Element of Sub U0 holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines Carr UNIALG_3:def 3 :

for U0 being Universal_Algebra

for b_{2} being Function of (Sub U0),(bool the carrier of U0) holds

( b_{2} = Carr U0 iff for u being Element of Sub U0 holds b_{2} . u = carr u );

for U0 being Universal_Algebra

for b

( b

theorem Th1: :: UNIALG_3:1

for U0 being Universal_Algebra

for u being object holds

( u in Sub U0 iff ex U1 being strict SubAlgebra of U0 st u = U1 )

for u being object holds

( u in Sub U0 iff ex U1 being strict SubAlgebra of U0 st u = U1 )

proof end;

theorem :: UNIALG_3:2

for U0 being Universal_Algebra

for H being non empty Subset of U0

for o being operation of U0 st arity o = 0 holds

( H is_closed_on o iff o . {} in H )

for H being non empty Subset of U0

for o being operation of U0 st arity o = 0 holds

( H is_closed_on o iff o . {} in H )

proof end;

theorem Th3: :: UNIALG_3:3

for U0 being Universal_Algebra

for U1 being SubAlgebra of U0 holds the carrier of U1 c= the carrier of U0

for U1 being SubAlgebra of U0 holds the carrier of U1 c= the carrier of U0

proof end;

theorem :: UNIALG_3:4

for U0 being Universal_Algebra

for H being non empty Subset of U0

for o being operation of U0 st H is_closed_on o & arity o = 0 holds

o /. H = o

for H being non empty Subset of U0

for o being operation of U0 st H is_closed_on o & arity o = 0 holds

o /. H = o

proof end;

theorem :: UNIALG_3:5

for U0 being Universal_Algebra holds Constants U0 = { (o . {}) where o is operation of U0 : arity o = 0 }

proof end;

theorem Th6: :: UNIALG_3:6

for U0 being with_const_op Universal_Algebra

for U1 being SubAlgebra of U0 holds Constants U0 = Constants U1

for U1 being SubAlgebra of U0 holds Constants U0 = Constants U1

proof end;

registration

let U0 be with_const_op Universal_Algebra;

coherence

for b_{1} being SubAlgebra of U0 holds b_{1} is with_const_op

end;
coherence

for b

proof end;

theorem :: UNIALG_3:7

for U0 being with_const_op Universal_Algebra

for U1, U2 being SubAlgebra of U0 holds Constants U1 = Constants U2

for U1, U2 being SubAlgebra of U0 holds Constants U1 = Constants U2

proof end;

definition

let U0 be Universal_Algebra;

for b_{1} being Function of (Sub U0),(bool the carrier of U0) holds

( b_{1} = Carr U0 iff for u being Element of Sub U0

for U1 being SubAlgebra of U0 st u = U1 holds

b_{1} . u = the carrier of U1 )

end;
redefine func Carr U0 means :Def4: :: UNIALG_3:def 4

for u being Element of Sub U0

for U1 being SubAlgebra of U0 st u = U1 holds

it . u = the carrier of U1;

compatibility for u being Element of Sub U0

for U1 being SubAlgebra of U0 st u = U1 holds

it . u = the carrier of U1;

for b

( b

for U1 being SubAlgebra of U0 st u = U1 holds

b

proof end;

:: deftheorem Def4 defines Carr UNIALG_3:def 4 :

for U0 being Universal_Algebra

for b_{2} being Function of (Sub U0),(bool the carrier of U0) holds

( b_{2} = Carr U0 iff for u being Element of Sub U0

for U1 being SubAlgebra of U0 st u = U1 holds

b_{2} . u = the carrier of U1 );

for U0 being Universal_Algebra

for b

( b

for U1 being SubAlgebra of U0 st u = U1 holds

b

theorem :: UNIALG_3:8

for U0 being Universal_Algebra

for H being strict SubAlgebra of U0

for u being Element of U0 holds

( u in (Carr U0) . H iff u in H )

for H being strict SubAlgebra of U0

for u being Element of U0 holds

( u in (Carr U0) . H iff u in H )

proof end;

theorem Th9: :: UNIALG_3:9

for U0 being Universal_Algebra

for H being non empty Subset of (Sub U0) holds not (Carr U0) .: H is empty

for H being non empty Subset of (Sub U0) holds not (Carr U0) .: H is empty

proof end;

theorem :: UNIALG_3:10

for U0 being with_const_op Universal_Algebra

for U1 being strict SubAlgebra of U0 holds Constants U0 c= (Carr U0) . U1

for U1 being strict SubAlgebra of U0 holds Constants U0 c= (Carr U0) . U1

proof end;

theorem Th11: :: UNIALG_3:11

for U0 being with_const_op Universal_Algebra

for U1 being SubAlgebra of U0

for a being set st a is Element of Constants U0 holds

a in the carrier of U1

for U1 being SubAlgebra of U0

for a being set st a is Element of Constants U0 holds

a in the carrier of U1

proof end;

theorem Th12: :: UNIALG_3:12

for U0 being with_const_op Universal_Algebra

for H being non empty Subset of (Sub U0) holds meet ((Carr U0) .: H) is non empty Subset of U0

for H being non empty Subset of (Sub U0) holds meet ((Carr U0) .: H) is non empty Subset of U0

proof end;

theorem :: UNIALG_3:13

theorem Th14: :: UNIALG_3:14

for U0 being with_const_op Universal_Algebra

for H being non empty Subset of (Sub U0)

for S being non empty Subset of U0 st S = meet ((Carr U0) .: H) holds

S is opers_closed

for H being non empty Subset of (Sub U0)

for S being non empty Subset of U0 st S = meet ((Carr U0) .: H) holds

S is opers_closed

proof end;

definition

let U0 be strict with_const_op Universal_Algebra;

let H be non empty Subset of (Sub U0);

ex b_{1} being strict SubAlgebra of U0 st the carrier of b_{1} = meet ((Carr U0) .: H)

for b_{1}, b_{2} being strict SubAlgebra of U0 st the carrier of b_{1} = meet ((Carr U0) .: H) & the carrier of b_{2} = meet ((Carr U0) .: H) holds

b_{1} = b_{2}
by UNIALG_2:12;

end;
let H be non empty Subset of (Sub U0);

func meet H -> strict SubAlgebra of U0 means :Def5: :: UNIALG_3:def 5

the carrier of it = meet ((Carr U0) .: H);

existence the carrier of it = meet ((Carr U0) .: H);

ex b

proof end;

uniqueness for b

b

:: deftheorem Def5 defines meet UNIALG_3:def 5 :

for U0 being strict with_const_op Universal_Algebra

for H being non empty Subset of (Sub U0)

for b_{3} being strict SubAlgebra of U0 holds

( b_{3} = meet H iff the carrier of b_{3} = meet ((Carr U0) .: H) );

for U0 being strict with_const_op Universal_Algebra

for H being non empty Subset of (Sub U0)

for b

( b

theorem Th15: :: UNIALG_3:15

for U0 being with_const_op Universal_Algebra

for l1, l2 being Element of (UnSubAlLattice U0)

for U1, U2 being strict SubAlgebra of U0 st l1 = U1 & l2 = U2 holds

( l1 [= l2 iff the carrier of U1 c= the carrier of U2 )

for l1, l2 being Element of (UnSubAlLattice U0)

for U1, U2 being strict SubAlgebra of U0 st l1 = U1 & l2 = U2 holds

( l1 [= l2 iff the carrier of U1 c= the carrier of U2 )

proof end;

theorem :: UNIALG_3:16

for U0 being with_const_op Universal_Algebra

for l1, l2 being Element of (UnSubAlLattice U0)

for U1, U2 being strict SubAlgebra of U0 st l1 = U1 & l2 = U2 holds

( l1 [= l2 iff U1 is SubAlgebra of U2 )

for l1, l2 being Element of (UnSubAlLattice U0)

for U1, U2 being strict SubAlgebra of U0 st l1 = U1 & l2 = U2 holds

( l1 [= l2 iff U1 is SubAlgebra of U2 )

proof end;

registration
end;

theorem Th18: :: UNIALG_3:18

for U0 being strict with_const_op Universal_Algebra

for U1 being strict SubAlgebra of U0 holds (GenUnivAlg (Constants U0)) /\ U1 = GenUnivAlg (Constants U0)

for U1 being strict SubAlgebra of U0 holds (GenUnivAlg (Constants U0)) /\ U1 = GenUnivAlg (Constants U0)

proof end;

theorem :: UNIALG_3:19

for U0 being strict with_const_op Universal_Algebra holds Bottom (UnSubAlLattice U0) = GenUnivAlg (Constants U0)

proof end;

theorem Th20: :: UNIALG_3:20

for U0 being strict with_const_op Universal_Algebra

for U1 being SubAlgebra of U0

for H being Subset of U0 st H = the carrier of U0 holds

(GenUnivAlg H) "\/" U1 = GenUnivAlg H

for U1 being SubAlgebra of U0

for H being Subset of U0 st H = the carrier of U0 holds

(GenUnivAlg H) "\/" U1 = GenUnivAlg H

proof end;

theorem Th21: :: UNIALG_3:21

for U0 being strict with_const_op Universal_Algebra

for H being Subset of U0 st H = the carrier of U0 holds

Top (UnSubAlLattice U0) = GenUnivAlg H

for H being Subset of U0 st H = the carrier of U0 holds

Top (UnSubAlLattice U0) = GenUnivAlg H

proof end;

definition

let U01, U02 be with_const_op Universal_Algebra;

let F be Function of the carrier of U01, the carrier of U02;

ex b_{1} being Function of the carrier of (UnSubAlLattice U01), the carrier of (UnSubAlLattice U02) st

for U1 being strict SubAlgebra of U01

for H being Subset of U02 st H = F .: the carrier of U1 holds

b_{1} . U1 = GenUnivAlg H

for b_{1}, b_{2} being Function of the carrier of (UnSubAlLattice U01), the carrier of (UnSubAlLattice U02) st ( for U1 being strict SubAlgebra of U01

for H being Subset of U02 st H = F .: the carrier of U1 holds

b_{1} . U1 = GenUnivAlg H ) & ( for U1 being strict SubAlgebra of U01

for H being Subset of U02 st H = F .: the carrier of U1 holds

b_{2} . U1 = GenUnivAlg H ) holds

b_{1} = b_{2}

end;
let F be Function of the carrier of U01, the carrier of U02;

func FuncLatt F -> Function of the carrier of (UnSubAlLattice U01), the carrier of (UnSubAlLattice U02) means :Def6: :: UNIALG_3:def 6

for U1 being strict SubAlgebra of U01

for H being Subset of U02 st H = F .: the carrier of U1 holds

it . U1 = GenUnivAlg H;

existence for U1 being strict SubAlgebra of U01

for H being Subset of U02 st H = F .: the carrier of U1 holds

it . U1 = GenUnivAlg H;

ex b

for U1 being strict SubAlgebra of U01

for H being Subset of U02 st H = F .: the carrier of U1 holds

b

proof end;

uniqueness for b

for H being Subset of U02 st H = F .: the carrier of U1 holds

b

for H being Subset of U02 st H = F .: the carrier of U1 holds

b

b

proof end;

:: deftheorem Def6 defines FuncLatt UNIALG_3:def 6 :

for U01, U02 being with_const_op Universal_Algebra

for F being Function of the carrier of U01, the carrier of U02

for b_{4} being Function of the carrier of (UnSubAlLattice U01), the carrier of (UnSubAlLattice U02) holds

( b_{4} = FuncLatt F iff for U1 being strict SubAlgebra of U01

for H being Subset of U02 st H = F .: the carrier of U1 holds

b_{4} . U1 = GenUnivAlg H );

for U01, U02 being with_const_op Universal_Algebra

for F being Function of the carrier of U01, the carrier of U02

for b

( b

for H being Subset of U02 st H = F .: the carrier of U1 holds

b

theorem :: UNIALG_3:24

for U0 being strict with_const_op Universal_Algebra

for F being Function of the carrier of U0, the carrier of U0 st F = id the carrier of U0 holds

FuncLatt F = id the carrier of (UnSubAlLattice U0)

for F being Function of the carrier of U0, the carrier of U0 st F = id the carrier of U0 holds

FuncLatt F = id the carrier of (UnSubAlLattice U0)

proof end;