:: YELLOW_2 semantic presentation

theorem Th1: :: YELLOW_2:1

for b₁ being non empty RelStr
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₃ c= downarrow b₂ iff b₃ is_<=_than b₂ )

proof end;

theorem Th2: :: YELLOW_2:2

for b₁ being non empty RelStr
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₃ c= uparrow b₂ iff b₂ is_<=_than b₃ )

proof end;

theorem Th3: :: YELLOW_2:3

for b₁ being transitive antisymmetric with_suprema RelStr
for b₂, b₃ being set st ex_sup_of b₂,b₁ & ex_sup_of b₃,b₁ holds
( ex_sup_of b₂ \/ b₃,b₁ & "\/" (b₂ \/ b₃),b₁ = ("\/" b₂,b₁) "\/" ("\/" b₃,b₁) )

proof end;

theorem Th4: :: YELLOW_2:4

for b₁ being transitive antisymmetric with_infima RelStr
for b₂, b₃ being set st ex_inf_of b₂,b₁ & ex_inf_of b₃,b₁ holds
( ex_inf_of b₂ \/ b₃,b₁ & "/\" (b₂ \/ b₃),b₁ = ("/\" b₂,b₁) "/\" ("/\" b₃,b₁) )

proof end;

theorem Th5: :: YELLOW_2:5

for b₁ being Relation
for b₂, b₃ being set st b₂ c= b₃ holds
b₁ |_2 b₂ c= b₁ |_2 b₃

proof end;

theorem Th6: :: YELLOW_2:6

for b₁ being RelStr
for b₂, b₃ being full SubRelStr of b₁ st the carrier of b₂ c= the carrier of b₃ holds
the InternalRel of b₂ c= the InternalRel of b₃

proof end;

theorem Th7: :: YELLOW_2:7

for b₁ being set
for b₂ being non empty RelStr
for b₃ being non empty SubRelStr of b₂ holds
( ( b₁ is directed Subset of b₃ implies b₁ is directed Subset of b₂ ) & ( b₁ is filtered Subset of b₃ implies b₁ is filtered Subset of b₂ ) )

proof end;

theorem Th8: :: YELLOW_2:8

for b₁ being non empty RelStr
for b₂, b₃ being non empty full SubRelStr of b₁ st the carrier of b₂ c= the carrier of b₃ holds
for b₄ being Subset of b₂ holds
( b₄ is Subset of b₃ & ( for b₅ being Subset of b₃ st b₄ = b₅ holds
( ( b₄ is filtered implies b₅ is filtered ) & ( b₄ is directed implies b₅ is directed ) ) ) )

proof end;

definition

let c₁, c₂ be 1-sorted ;
let c₃ be Function of c₁,c₂;
redefine func rng as rng c₃ -> Subset of a₂;
coherence by RELSET_1:12;

end;

definition

let c₁ be set ;
let c₂ be RelStr ;
let c₃, c₄ be Function of c₁,the carrier of c₂;
pred c₃ <= c₄ means :Def1: :: YELLOW_2:def 1
for b₁ being set st b₁ in a₁ holds
ex b₂, b₃ being Element of a₂ st
( b₂ = a₃ . b₁ & b₃ = a₄ . b₁ & b₂ <= b₃ );

end;

:: deftheorem Def1 defines <= YELLOW_2:def 1 :

notation

let c₁ be set ;
let c₂ be RelStr ;
let c₃, c₄ be Function of c₁,the carrier of c₂;
synonym c₄ >= c₃ for c₃ <= c₄;

end;

theorem Th9: :: YELLOW_2:9

canceled;

theorem Th10: :: YELLOW_2:10

for b₁, b₂ being non empty RelStr
for b₃, b₄ being Function of b₁,b₂ holds
( b₃ <= b₄ iff for b₅ being Element of b₁ holds b₃ . b₅ <= b₄ . b₅ )

proof end;

definition

let c₁, c₂ be non empty RelStr ;
let c₃ be Function of c₁,c₂;
func Image c₃ -> strict full SubRelStr of a₂ equals :: YELLOW_2:def 2
subrelstr (rng a₃);
correctness ;

end;

:: deftheorem Def2 defines Image YELLOW_2:def 2 :

theorem Th11: :: YELLOW_2:11

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂ holds rng b₃ = the carrier of (Image b₃) by YELLOW_0:def 15;

theorem Th12: :: YELLOW_2:12

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂
for b₄ being Element of (Image b₃) ex b₅ being Element of b₁ st b₃ . b₅ = b₄

proof end;

registration

let c₁ be non empty RelStr ;
let c₂ be non empty Subset of c₁;
cluster subrelstr a₂ -> non empty ;
coherence

proof end;

end;

registration

let c₁, c₂ be non empty RelStr ;
let c₃ be Function of c₁,c₂;
cluster Image a₃ -> non empty strict full ;
coherence

proof end;

end;

theorem Th13: :: YELLOW_2:13

for b₁ being non empty RelStr holds id b₁ is monotone

proof end;

theorem Th14: :: YELLOW_2:14

for b₁, b₂, b₃ being non empty RelStr
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st b₄ is monotone & b₅ is monotone holds
b₅ * b₄ is monotone

proof end;

theorem Th15: :: YELLOW_2:15

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂
for b₄ being Subset of b₁
for b₅ being Element of b₁ st b₃ is monotone & b₅ is_<=_than b₄ holds
b₃ . b₅ is_<=_than b₃ .: b₄

proof end;

theorem Th16: :: YELLOW_2:16

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂
for b₄ being Subset of b₁
for b₅ being Element of b₁ st b₃ is monotone & b₄ is_<=_than b₅ holds
b₃ .: b₄ is_<=_than b₃ . b₅

proof end;

theorem Th17: :: YELLOW_2:17

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂
for b₄ being directed Subset of b₁ st b₃ is monotone holds
b₃ .: b₄ is directed

proof end;

theorem Th18: :: YELLOW_2:18

for b₁ being with_suprema Poset
for b₂ being Function of b₁,b₁ st b₂ is directed-sups-preserving holds
b₂ is monotone

proof end;

theorem Th19: :: YELLOW_2:19

for b₁ being with_infima Poset
for b₂ being Function of b₁,b₁ st b₂ is filtered-infs-preserving holds
b₂ is monotone

proof end;

theorem Th20: :: YELLOW_2:20

for b₁ being non empty 1-sorted
for b₂ being Function of b₁,b₁ st b₂ is idempotent holds
for b₃ being Element of b₁ holds b₂ . (b₂ . b₃) = b₂ . b₃

proof end;

theorem Th21: :: YELLOW_2:21

for b₁ being non empty 1-sorted
for b₂ being Function of b₁,b₁ st b₂ is idempotent holds
rng b₂ = { b₃ where B is Element of b₁ : b₃ = b₂ . b₃ }

proof end;

theorem Th22: :: YELLOW_2:22

for b₁ being set
for b₂ being non empty 1-sorted
for b₃ being Function of b₂,b₂ st b₃ is idempotent & b₁ c= rng b₃ holds
b₃ .: b₁ = b₁

proof end;

theorem Th23: :: YELLOW_2:23

for b₁ being non empty RelStr holds id b₁ is idempotent

proof end;

theorem Th24: :: YELLOW_2:24

for b₁ being set
for b₂ being complete LATTICE
for b₃ being Element of b₂ st b₃ in b₁ holds
( b₃ <= "\/" b₁,b₂ & "/\" b₁,b₂ <= b₃ )

proof end;

theorem Th25: :: YELLOW_2:25

for b₁ being non empty RelStr holds
( ( for b₂ being set holds ex_sup_of b₂,b₁ ) iff for b₂ being set holds ex_inf_of b₂,b₁ )

proof end;

theorem Th26: :: YELLOW_2:26

for b₁ being non empty RelStr st ( for b₂ being set holds ex_sup_of b₂,b₁ ) holds
b₁ is complete

proof end;

theorem Th27: :: YELLOW_2:27

for b₁ being non empty RelStr st ( for b₂ being set holds ex_inf_of b₂,b₁ ) holds
b₁ is complete

proof end;

theorem Th28: :: YELLOW_2:28

for b₁ being non empty RelStr st ( for b₂ being Subset of b₁ holds ex_inf_of b₂,b₁ ) holds
for b₂ being set holds
( ex_inf_of b₂,b₁ & "/\" b₂,b₁ = "/\" (b₂ /\ the carrier of b₁),b₁ )

proof end;

theorem Th29: :: YELLOW_2:29

for b₁ being non empty RelStr st ( for b₂ being Subset of b₁ holds ex_sup_of b₂,b₁ ) holds
for b₂ being set holds
( ex_sup_of b₂,b₁ & "\/" b₂,b₁ = "\/" (b₂ /\ the carrier of b₁),b₁ )

proof end;

theorem Th30: :: YELLOW_2:30

for b₁ being non empty RelStr st ( for b₂ being Subset of b₁ holds ex_inf_of b₂,b₁ ) holds
b₁ is complete

proof end;

Lemma14: for b₁ being non empty Poset st b₁ is up-complete & b₁ is /\-complete & b₁ is upper-bounded holds
b₁ is non empty complete Poset

proof end;

registration

cluster non empty upper-bounded up-complete /\-complete -> non empty complete RelStr ;
correctness by Lemma14;

end;

theorem Th31: :: YELLOW_2:31

for b₁ being complete LATTICE
for b₂ being Function of b₁,b₁ st b₂ is monotone holds
for b₃ being Subset of b₁ st b₃ = { b₄ where B is Element of b₁ : b₄ = b₂ . b₄ } holds
subrelstr b₃ is complete LATTICE

proof end;

theorem Th32: :: YELLOW_2:32

for b₁ being complete LATTICE
for b₂ being non empty full infs-inheriting SubRelStr of b₁ holds b₂ is complete LATTICE

proof end;

theorem Th33: :: YELLOW_2:33

for b₁ being complete LATTICE
for b₂ being non empty full sups-inheriting SubRelStr of b₁ holds b₂ is complete LATTICE

proof end;

theorem Th34: :: YELLOW_2:34

for b₁ being complete LATTICE
for b₂ being non empty RelStr
for b₃ being Function of b₁,b₂ st b₃ is sups-preserving holds
Image b₃ is sups-inheriting

proof end;

theorem Th35: :: YELLOW_2:35

for b₁ being complete LATTICE
for b₂ being non empty RelStr
for b₃ being Function of b₁,b₂ st b₃ is infs-preserving holds
Image b₃ is infs-inheriting

proof end;

theorem Th36: :: YELLOW_2:36

for b₁, b₂ being complete LATTICE
for b₃ being Function of b₁,b₂ st ( b₃ is sups-preserving or b₃ is infs-preserving ) holds
Image b₃ is complete LATTICE

proof end;

theorem Th37: :: YELLOW_2:37

for b₁ being complete LATTICE
for b₂ being Function of b₁,b₁ st b₂ is idempotent & b₂ is directed-sups-preserving holds
( Image b₂ is directed-sups-inheriting & Image b₂ is complete LATTICE )

proof end;

theorem Th38: :: YELLOW_2:38

for b₁ being RelStr
for b₂ being Subset-Family of b₁ st ( for b₃ being Subset of b₁ st b₃ in b₂ holds
b₃ is lower ) holds
meet b₂ is lower Subset of b₁

proof end;

theorem Th39: :: YELLOW_2:39

for b₁ being RelStr
for b₂ being Subset-Family of b₁ st ( for b₃ being Subset of b₁ st b₃ in b₂ holds
b₃ is upper ) holds
meet b₂ is upper Subset of b₁

proof end;

theorem Th40: :: YELLOW_2:40

for b₁ being antisymmetric with_suprema RelStr
for b₂ being Subset-Family of b₁ st ( for b₃ being Subset of b₁ st b₃ in b₂ holds
( b₃ is lower & b₃ is directed ) ) holds
meet b₂ is directed Subset of b₁

proof end;

theorem Th41: :: YELLOW_2:41

for b₁ being antisymmetric with_infima RelStr
for b₂ being Subset-Family of b₁ st ( for b₃ being Subset of b₁ st b₃ in b₂ holds
( b₃ is upper & b₃ is filtered ) ) holds
meet b₂ is filtered Subset of b₁

proof end;

theorem Th42: :: YELLOW_2:42

for b₁ being with_infima Poset
for b₂, b₃ being Ideal of b₁ holds b₂ /\ b₃ is Ideal of b₁

proof end;

registration

let c₁ be non empty reflexive transitive RelStr ;
cluster Ids a₁ -> non empty ;
correctness

proof end;

end;

theorem Th43: :: YELLOW_2:43

for b₁ being set
for b₂ being non empty reflexive transitive RelStr holds
( b₁ is Element of (InclPoset (Ids b₂)) iff b₁ is Ideal of b₂ )

proof end;

theorem Th44: :: YELLOW_2:44

for b₁ being set
for b₂ being non empty reflexive transitive RelStr
for b₃ being Element of (InclPoset (Ids b₂)) st b₁ in b₃ holds
b₁ is Element of b₂

proof end;

theorem Th45: :: YELLOW_2:45

for b₁ being with_infima Poset
for b₂, b₃ being Element of (InclPoset (Ids b₁)) holds b₂ "/\" b₃ = b₂ /\ b₃

proof end;

registration

let c₁ be with_infima Poset;
cluster InclPoset (Ids a₁) -> with_infima ;
correctness

proof end;

end;

theorem Th46: :: YELLOW_2:46

for b₁ being with_suprema Poset
for b₂, b₃ being Element of (InclPoset (Ids b₁)) ex b₄ being Subset of b₁ st
( b₄ = { b₅ where B is Element of b₁ : ( b₅ in b₂ or b₅ in b₃ or ex b₁, b₂ being Element of b₁ st
( b₆ in b₂ & b₇ in b₃ & b₅ = b₆ "\/" b₇ ) ) } & ex_sup_of {b₂,b₃}, InclPoset (Ids b₁) & b₂ "\/" b₃ = downarrow b₄ )

proof end;

registration

let c₁ be with_suprema Poset;
cluster InclPoset (Ids a₁) -> with_suprema ;
correctness

proof end;

end;

theorem Th47: :: YELLOW_2:47

for b₁ being lower-bounded sup-Semilattice
for b₂ being non empty Subset of (Ids b₁) holds meet b₂ is Ideal of b₁

proof end;

theorem Th48: :: YELLOW_2:48

for b₁ being lower-bounded sup-Semilattice
for b₂ being non empty Subset of (InclPoset (Ids b₁)) holds
( ex_inf_of b₂, InclPoset (Ids b₁) & inf b₂ = meet b₂ )

proof end;

theorem Th49: :: YELLOW_2:49

for b₁ being with_suprema Poset holds
( ex_inf_of {} , InclPoset (Ids b₁) & "/\" {} ,(InclPoset (Ids b₁)) = [#] b₁ )

proof end;

theorem Th50: :: YELLOW_2:50

for b₁ being lower-bounded sup-Semilattice holds InclPoset (Ids b₁) is complete

proof end;

registration

let c₁ be lower-bounded sup-Semilattice;
cluster InclPoset (Ids a₁) -> with_suprema complete ;
correctness by Th50;

end;

definition

let c₁ be non empty Poset;
func SupMap c₁ -> Function of (InclPoset (Ids a₁)),a₁ means :Def3: :: YELLOW_2:def 3
for b₁ being Ideal of a₁ holds a₂ . b₁ = sup b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines SupMap YELLOW_2:def 3 :

theorem Th51: :: YELLOW_2:51

for b₁ being non empty Poset holds
( dom (SupMap b₁) = Ids b₁ & rng (SupMap b₁) is Subset of b₁ )

proof end;

theorem Th52: :: YELLOW_2:52

for b₁ being set
for b₂ being non empty Poset holds
( b₁ in dom (SupMap b₂) iff b₁ is Ideal of b₂ )

proof end;

theorem Th53: :: YELLOW_2:53

for b₁ being non empty up-complete Poset holds SupMap b₁ is monotone

proof end;

registration

let c₁ be non empty up-complete Poset;
cluster SupMap a₁ -> monotone ;
correctness by Th53;

end;

definition

let c₁ be non empty Poset;
func IdsMap c₁ -> Function of a₁,(InclPoset (Ids a₁)) means :Def4: :: YELLOW_2:def 4
for b₁ being Element of a₁ holds a₂ . b₁ = downarrow b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines IdsMap YELLOW_2:def 4 :

theorem Th54: :: YELLOW_2:54

for b₁ being non empty Poset holds IdsMap b₁ is monotone

proof end;

registration

let c₁ be non empty Poset;
cluster IdsMap a₁ -> monotone ;
correctness by Th54;

end;

definition

let c₁ be non empty RelStr ;
let c₂ be Relation;
func \\/ c₂,c₁ -> Element of a₁ equals :: YELLOW_2:def 5
"\/" (rng a₂),a₁;
coherence ;
func //\ c₂,c₁ -> Element of a₁ equals :: YELLOW_2:def 6
"/\" (rng a₂),a₁;
coherence ;

end;

:: deftheorem Def5 defines \\/ YELLOW_2:def 5 :

:: deftheorem Def6 defines //\ YELLOW_2:def 6 :

notation

let c₁ be set ;
let c₂ be non empty RelStr ;
let c₃ be Function of c₁,the carrier of c₂;
synonym Sup c₃ for \\/ c₂,c₁;
synonym Inf c₃ for //\ c₂,c₁;

end;

definition

let c₁ be non empty set ;
let c₂ be non empty 1-sorted ;
let c₃ be Function of c₁,the carrier of c₂;
let c₄ be Element of c₁;
redefine func . as c₃ . c₄ -> Element of a₂;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be non empty 1-sorted ;
let c₃ be Function of c₁,the carrier of c₂;
redefine func rng as rng c₃ -> Subset of a₂;
coherence by RELSET_1:12;

end;

theorem Th55: :: YELLOW_2:55

for b₁ being complete LATTICE
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being Function of b₂,the carrier of b₁ holds
( b₄ . b₃ <= Sup & Inf <= b₄ . b₃ )

proof end;

theorem Th56: :: YELLOW_2:56

for b₁ being complete LATTICE
for b₂ being Element of b₁
for b₃ being non empty set
for b₄ being Function of b₃,the carrier of b₁ st ( for b₅ being Element of b₃ holds b₄ . b₅ <= b₂ ) holds
Sup <= b₂

proof end;

theorem Th57: :: YELLOW_2:57

for b₁ being complete LATTICE
for b₂ being Element of b₁
for b₃ being non empty set
for b₄ being Function of b₃,the carrier of b₁ st ( for b₅ being Element of b₃ holds b₂ <= b₄ . b₅ ) holds
b₂ <= Inf

proof end;