:: YELLOW_1 semantic presentation

registration

let c₁ be Lattice;
cluster LattPOSet a₁ -> with_suprema with_infima ;
coherence by LATTICE3:11;

end;

registration

let c₁ be upper-bounded Lattice;
cluster LattPOSet a₁ -> upper-bounded with_suprema with_infima ;
coherence

proof end;

end;

registration

let c₁ be lower-bounded Lattice;
cluster LattPOSet a₁ -> lower-bounded with_suprema with_infima ;
coherence

proof end;

end;

registration

let c₁ be complete Lattice;
cluster LattPOSet a₁ -> lower-bounded upper-bounded with_suprema with_infima complete ;
coherence

proof end;

end;

definition

let c₁ be set ;
redefine func RelIncl as RelIncl c₁ -> Order of a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
func InclPoset c₁ -> strict RelStr equals :: YELLOW_1:def 1
RelStr(# a₁,(RelIncl a₁) #);
correctness ;

end;

:: deftheorem Def1 defines InclPoset YELLOW_1:def 1 :

registration

let c₁ be set ;
cluster InclPoset a₁ -> strict reflexive transitive antisymmetric ;
coherence ;

end;

registration

let c₁ be non empty set ;
cluster InclPoset a₁ -> non empty strict reflexive transitive antisymmetric ;
coherence ;

end;

theorem Th1: :: YELLOW_1:1

for b₁ being set holds
( the carrier of (InclPoset b₁) = b₁ & the InternalRel of (InclPoset b₁) = RelIncl b₁ ) ;

definition

let c₁ be set ;
func BoolePoset c₁ -> strict RelStr equals :: YELLOW_1:def 2
LattPOSet (BooleLatt a₁);
correctness ;

end;

:: deftheorem Def2 defines BoolePoset YELLOW_1:def 2 :

registration

let c₁ be set ;
cluster BoolePoset a₁ -> non empty strict reflexive transitive antisymmetric ;
coherence ;

end;

registration

let c₁ be set ;
cluster BoolePoset a₁ -> non empty strict reflexive transitive antisymmetric complete ;
coherence ;

end;

theorem Th2: :: YELLOW_1:2

for b₁ being set
for b₂, b₃ being Element of (BoolePoset b₁) holds
( b₂ <= b₃ iff b₂ c= b₃ )

proof end;

theorem Th3: :: YELLOW_1:3

for b₁ being non empty set
for b₂, b₃ being Element of (InclPoset b₁) holds
( b₂ <= b₃ iff b₂ c= b₃ )

proof end;

theorem Th4: :: YELLOW_1:4

for b₁ being set holds BoolePoset b₁ = InclPoset (bool b₁)

proof end;

theorem Th5: :: YELLOW_1:5

for b₁ being set
for b₂ being Subset-Family of b₁ holds InclPoset b₂ is full SubRelStr of BoolePoset b₁

proof end;

theorem Th6: :: YELLOW_1:6

for b₁ being non empty set st InclPoset b₁ is with_suprema holds
for b₂, b₃ being Element of (InclPoset b₁) holds b₂ \/ b₃ c= b₂ "\/" b₃

proof end;

theorem Th7: :: YELLOW_1:7

for b₁ being non empty set st InclPoset b₁ is with_infima holds
for b₂, b₃ being Element of (InclPoset b₁) holds b₂ "/\" b₃ c= b₂ /\ b₃

proof end;

theorem Th8: :: YELLOW_1:8

for b₁ being non empty set
for b₂, b₃ being Element of (InclPoset b₁) st b₂ \/ b₃ in b₁ holds
b₂ "\/" b₃ = b₂ \/ b₃

proof end;

theorem Th9: :: YELLOW_1:9

for b₁ being non empty set
for b₂, b₃ being Element of (InclPoset b₁) st b₂ /\ b₃ in b₁ holds
b₂ "/\" b₃ = b₂ /\ b₃

proof end;

theorem Th10: :: YELLOW_1:10

for b₁ being RelStr st ( for b₂, b₃ being Element of b₁ holds
( b₂ <= b₃ iff b₂ c= b₃ ) ) holds
the InternalRel of b₁ = RelIncl the carrier of b₁

proof end;

theorem Th11: :: YELLOW_1:11

for b₁ being non empty set st ( for b₂, b₃ being set st b₂ in b₁ & b₃ in b₁ holds
b₂ \/ b₃ in b₁ ) holds
InclPoset b₁ is with_suprema

proof end;

theorem Th12: :: YELLOW_1:12

for b₁ being non empty set st ( for b₂, b₃ being set st b₂ in b₁ & b₃ in b₁ holds
b₂ /\ b₃ in b₁ ) holds
InclPoset b₁ is with_infima

proof end;

theorem Th13: :: YELLOW_1:13

for b₁ being non empty set st {} in b₁ holds
Bottom (InclPoset b₁) = {}

proof end;

theorem Th14: :: YELLOW_1:14

for b₁ being non empty set st union b₁ in b₁ holds
Top (InclPoset b₁) = union b₁

proof end;

theorem Th15: :: YELLOW_1:15

for b₁ being non empty set st InclPoset b₁ is upper-bounded holds
union b₁ in b₁

proof end;

theorem Th16: :: YELLOW_1:16

for b₁ being non empty set st InclPoset b₁ is lower-bounded holds
meet b₁ in b₁

proof end;

Lemma8: for b₁ being set holds the carrier of (BoolePoset b₁) = bool b₁
by LATTICE3:def 1;

Lemma9: for b₁ being set
for b₂, b₃ being Element of (BoolePoset b₁) holds
( b₂ /\ b₃ in bool b₁ & b₂ \/ b₃ in bool b₁ )

proof end;

theorem Th17: :: YELLOW_1:17

for b₁ being set
for b₂, b₃ being Element of (BoolePoset b₁) holds
( b₂ "\/" b₃ = b₂ \/ b₃ & b₂ "/\" b₃ = b₂ /\ b₃ )

proof end;

theorem Th18: :: YELLOW_1:18

for b₁ being set holds Bottom (BoolePoset b₁) = {}

proof end;

theorem Th19: :: YELLOW_1:19

for b₁ being set holds Top (BoolePoset b₁) = b₁

proof end;

theorem Th20: :: YELLOW_1:20

for b₁ being set
for b₂ being non empty Subset of (BoolePoset b₁) holds inf b₂ = meet b₂

proof end;

theorem Th21: :: YELLOW_1:21

for b₁ being set
for b₂ being Subset of (BoolePoset b₁) holds sup b₂ = union b₂

proof end;

theorem Th22: :: YELLOW_1:22

for b₁ being non empty TopSpace
for b₂ being Subset of (InclPoset the topology of b₁) holds sup b₂ = union b₂

proof end;

theorem Th23: :: YELLOW_1:23

for b₁ being non empty TopSpace holds Bottom (InclPoset the topology of b₁) = {}

proof end;

Lemma10: for b₁ being non empty TopSpace holds InclPoset the topology of b₁ is lower-bounded

proof end;

theorem Th24: :: YELLOW_1:24

for b₁ being non empty TopSpace holds Top (InclPoset the topology of b₁) = the carrier of b₁

proof end;

Lemma11: for b₁ being non empty TopSpace holds InclPoset the topology of b₁ is complete

proof end;

Lemma12: for b₁ being non empty TopSpace holds not InclPoset the topology of b₁ is trivial

proof end;

registration

let c₁ be non empty TopSpace;
cluster InclPoset the topology of a₁ -> non empty strict reflexive transitive antisymmetric complete non trivial ;
coherence by Lemma11, Lemma12;

end;

theorem Th25: :: YELLOW_1:25

for b₁ being TopSpace
for b₂ being Subset-Family of b₁ holds
( b₂ is open iff b₂ is Subset of (InclPoset the topology of b₁) )

proof end;

definition

let c₁ be Relation;
attr a₁ is RelStr-yielding means :Def3: :: YELLOW_1:def 3
for b₁ being set st b₁ in rng a₁ holds
b₁ is RelStr ;

end;

:: deftheorem Def3 defines RelStr-yielding YELLOW_1:def 3 :

registration

cluster RelStr-yielding -> 1-sorted-yielding set ;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster 1-sorted-yielding RelStr-yielding ManySortedSet of a₁;
existence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be RelStr-yielding ManySortedSet of c₁;
let c₃ be Element of c₁;
redefine func . as c₂ . c₃ -> RelStr ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be RelStr-yielding ManySortedSet of c₁;
func product c₂ -> strict RelStr means :Def4: :: YELLOW_1:def 4
( the carrier of a₃ = product (Carrier a₂) & ( for b₁, b₂ being Element of a₃ st b₁ in product (Carrier a₂) holds
( b₁ <= b₂ iff ex b₃, b₄ being Function st
( b₃ = b₁ & b₄ = b₂ & ( for b₅ being set st b₅ in a₁ holds
ex b₆ being RelStr ex b₇, b₈ being Element of b₆ st
( b₆ = a₂ . b₅ & b₇ = b₃ . b₅ & b₈ = b₄ . b₅ & b₇ <= b₈ ) ) ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines product YELLOW_1:def 4 :

registration

let c₁ be set ;
let c₂ be RelStr ;
cluster K134(a₁,a₂) -> 1-sorted-yielding RelStr-yielding ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be RelStr ;
func c₂ |^ c₁ -> strict RelStr equals :: YELLOW_1:def 5
product (a₁ --> a₂);
correctness ;

end;

:: deftheorem Def5 defines |^ YELLOW_1:def 5 :

theorem Th26: :: YELLOW_1:26

for b₁ being RelStr-yielding ManySortedSet of {} holds product b₁ = RelStr(# {{} },(id {{} }) #)

proof end;

theorem Th27: :: YELLOW_1:27

for b₁ being RelStr holds b₁ |^ {} = RelStr(# {{} },(id {{} }) #) by Th26;

theorem Th28: :: YELLOW_1:28

for b₁ being set
for b₂ being RelStr holds Funcs b₁,the carrier of b₂ = the carrier of (b₂ |^ b₁)

proof end;

registration

let c₁ be set ;
let c₂ be non empty RelStr ;
cluster a₂ |^ a₁ -> non empty strict ;
coherence

proof end;

end;

Lemma18: for b₁ being set
for b₂ being non empty RelStr
for b₃ being Element of (b₂ |^ b₁) holds
( b₃ in the carrier of (product (b₁ --> b₂)) & b₃ is Function of b₁,the carrier of b₂ )

proof end;

registration

let c₁ be set ;
let c₂ be non empty reflexive RelStr ;
cluster a₂ |^ a₁ -> non empty strict reflexive ;
coherence

proof end;

end;

registration

let c₁ be non empty RelStr ;
cluster a₁ |^ {} -> non empty strict trivial ;
coherence by Th27;

end;

registration

let c₁ be non empty reflexive RelStr ;
cluster a₁ |^ {} -> non empty strict reflexive antisymmetric with_suprema with_infima trivial ;
coherence ;

end;

registration

let c₁ be set ;
let c₂ be non empty transitive RelStr ;
cluster a₂ |^ a₁ -> non empty strict transitive ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be non empty antisymmetric RelStr ;
cluster a₂ |^ a₁ -> non empty strict antisymmetric ;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be non empty antisymmetric with_infima RelStr ;
cluster a₂ |^ a₁ -> non empty strict antisymmetric with_infima ;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be non empty antisymmetric with_suprema RelStr ;
cluster a₂ |^ a₁ -> non empty strict antisymmetric with_suprema ;
coherence

proof end;

end;

definition

let c₁, c₂ be RelStr ;
func MonMaps c₁,c₂ -> strict full SubRelStr of a₂ |^ the carrier of a₁ means :: YELLOW_1:def 6
for b₁ being Function of a₁,a₂ holds
( b₁ in the carrier of a₃ iff ( b₁ in Funcs the carrier of a₁,the carrier of a₂ & b₁ is monotone ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines MonMaps YELLOW_1:def 6 :