:: YELLOW_1 semantic presentation

registration

let L be Lattice;
cluster LattPOSet L -> with_suprema with_infima ;
coherence by LATTICE3:11;

end;

registration

let L be upper-bounded Lattice;
cluster LattPOSet L -> upper-bounded with_suprema with_infima ;
coherence

proof end;

end;

registration

let L be lower-bounded Lattice;
cluster LattPOSet L -> lower-bounded with_suprema with_infima ;
coherence

proof end;

end;

registration

let L be complete Lattice;
cluster LattPOSet L -> lower-bounded upper-bounded with_suprema with_infima complete ;
coherence

proof end;

end;

definition

let X be set ;
:: original: RelIncl
redefine func RelIncl X -> Order of X;
coherence

proof end;

end;

definition

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

end;

:: deftheorem defines InclPoset YELLOW_1:def 1 :

registration

let X be set ;
cluster InclPoset X -> strict reflexive transitive antisymmetric ;
coherence ;

end;

registration

let X be non empty set ;
cluster InclPoset X -> non empty strict reflexive transitive antisymmetric ;
coherence ;

end;

theorem :: YELLOW_1:1

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

definition

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

end;

:: deftheorem defines BoolePoset YELLOW_1:def 2 :

registration

let X be set ;
cluster BoolePoset X -> non empty strict reflexive transitive antisymmetric ;
coherence ;

end;

registration

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

end;

theorem Th2: :: YELLOW_1:2

for X being set
for x, y being Element of (BoolePoset X) holds
( x <= y iff x c= y )

proof end;

theorem Th3: :: YELLOW_1:3

for X being non empty set
for x, y being Element of (InclPoset X) holds
( x <= y iff x c= y )

proof end;

theorem Th4: :: YELLOW_1:4

for X being set holds BoolePoset X = InclPoset (bool X)

proof end;

theorem :: YELLOW_1:5

for X being set
for Y being Subset-Family of X holds InclPoset Y is full SubRelStr of BoolePoset X

proof end;

theorem :: YELLOW_1:6

for X being non empty set st InclPoset X is with_suprema holds
for x, y being Element of (InclPoset X) holds x \/ y c= x "\/" y

proof end;

theorem :: YELLOW_1:7

for X being non empty set st InclPoset X is with_infima holds
for x, y being Element of (InclPoset X) holds x "/\" y c= x /\ y

proof end;

theorem Th8: :: YELLOW_1:8

for X being non empty set
for x, y being Element of (InclPoset X) st x \/ y in X holds
x "\/" y = x \/ y

proof end;

theorem Th9: :: YELLOW_1:9

for X being non empty set
for x, y being Element of (InclPoset X) st x /\ y in X holds
x "/\" y = x /\ y

proof end;

theorem :: YELLOW_1:10

for L being RelStr st ( for x, y being Element of L holds
( x <= y iff x c= y ) ) holds
the InternalRel of L = RelIncl the carrier of L

proof end;

theorem :: YELLOW_1:11

for X being non empty set st ( for x, y being set st x in X & y in X holds
x \/ y in X ) holds
InclPoset X is with_suprema

proof end;

theorem :: YELLOW_1:12

for X being non empty set st ( for x, y being set st x in X & y in X holds
x /\ y in X ) holds
InclPoset X is with_infima

proof end;

theorem Th13: :: YELLOW_1:13

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

proof end;

theorem Th14: :: YELLOW_1:14

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

proof end;

theorem :: YELLOW_1:15

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

proof end;

theorem :: YELLOW_1:16

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

proof end;

Lm1: for X being set holds the carrier of (BoolePoset X) = bool X
by LATTICE3:def 1;

Lm2: for X being set
for x, y being Element of (BoolePoset X) holds
( x /\ y in bool X & x \/ y in bool X )

proof end;

theorem :: YELLOW_1:17

for X being set
for x, y being Element of (BoolePoset X) holds
( x "\/" y = x \/ y & x "/\" y = x /\ y )

proof end;

theorem :: YELLOW_1:18

for X being set holds Bottom (BoolePoset X) = {}

proof end;

theorem :: YELLOW_1:19

for X being set holds Top (BoolePoset X) = X

proof end;

theorem :: YELLOW_1:20

for X being set
for Y being non empty Subset of (BoolePoset X) holds inf Y = meet Y

proof end;

theorem :: YELLOW_1:21

for X being set
for Y being Subset of (BoolePoset X) holds sup Y = union Y

proof end;

theorem :: YELLOW_1:22

for T being non empty TopSpace
for X being Subset of (InclPoset the topology of T) holds sup X = union X

proof end;

theorem :: YELLOW_1:23

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

proof end;

Lm3: for T being non empty TopSpace holds InclPoset the topology of T is lower-bounded

proof end;

theorem :: YELLOW_1:24

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

proof end;

Lm4: for T being non empty TopSpace holds InclPoset the topology of T is complete

proof end;

Lm5: for T being non empty TopSpace holds not InclPoset the topology of T is trivial

proof end;

registration

let T be non empty TopSpace;
cluster InclPoset the topology of T -> non empty strict reflexive transitive antisymmetric complete non trivial ;
coherence by Lm4, Lm5;

end;

theorem :: YELLOW_1:25

for T being TopSpace
for F being Subset-Family of T holds
( F is open iff F is Subset of (InclPoset the topology of T) )

proof end;

definition

let R be Relation;
attr R is RelStr-yielding means :Def3: :: YELLOW_1:def 3
for v being set st v in rng R holds
v 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 I be set ;
cluster 1-sorted-yielding RelStr-yielding ManySortedSet of I;
existence

proof end;

end;

definition

let J be non empty set ;
let A be RelStr-yielding ManySortedSet of J;
let j be Element of J;
:: original: .
redefine func A . j -> RelStr ;
coherence

proof end;

end;

definition

let I be set ;
let J be RelStr-yielding ManySortedSet of I;
func product J -> strict RelStr means :Def4: :: YELLOW_1:def 4
( the carrier of it = product (Carrier J) & ( for x, y being Element of it st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines product YELLOW_1:def 4 :

registration

let X be set ;
let L be RelStr ;
cluster K134(X,L) -> 1-sorted-yielding RelStr-yielding ;
coherence

proof end;

end;

definition

let I be set ;
let T be RelStr ;
func T |^ I -> strict RelStr equals :: YELLOW_1:def 5
product (I --> T);
correctness ;

end;

:: deftheorem defines |^ YELLOW_1:def 5 :

theorem Th26: :: YELLOW_1:26

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

proof end;

theorem Th27: :: YELLOW_1:27

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

theorem Th28: :: YELLOW_1:28

for X being set
for Y being RelStr holds Funcs X,the carrier of Y = the carrier of (Y |^ X)

proof end;

registration

let X be set ;
let Y be non empty RelStr ;
cluster Y |^ X -> non empty strict ;
coherence

proof end;

end;

Lm6: for X being set
for Y being non empty RelStr
for x being Element of (Y |^ X) holds
( x in the carrier of (product (X --> Y)) & x is Function of X,the carrier of Y )

proof end;

registration

let X be set ;
let Y be non empty reflexive RelStr ;
cluster Y |^ X -> non empty strict reflexive ;
coherence

proof end;

end;

registration

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

end;

registration

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

end;

registration

let X be set ;
let Y be non empty transitive RelStr ;
cluster Y |^ X -> non empty strict transitive ;
coherence

proof end;

end;

registration

let X be set ;
let Y be non empty antisymmetric RelStr ;
cluster Y |^ X -> non empty strict antisymmetric ;
coherence

proof end;

end;

registration

let X be non empty set ;
let Y be non empty antisymmetric with_infima RelStr ;
cluster Y |^ X -> non empty strict antisymmetric with_infima ;
coherence

proof end;

end;

registration

let X be non empty set ;
let Y be non empty antisymmetric with_suprema RelStr ;
cluster Y |^ X -> non empty strict antisymmetric with_suprema ;
coherence

proof end;

end;

definition

let S, T be RelStr ;
func MonMaps S,T -> strict full SubRelStr of T |^ the carrier of S means :: YELLOW_1:def 6
for f being Function of S,T holds
( f in the carrier of it iff ( f in Funcs the carrier of S,the carrier of T & f is monotone ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines MonMaps YELLOW_1:def 6 :