:: WAYBEL_0 semantic presentation

definition

let c₁ be RelStr ;
let c₂ be Subset of c₁;
attr a₂ is directed means :Def1: :: WAYBEL_0:def 1
for b₁, b₂ being Element of a₁ st b₁ in a₂ & b₂ in a₂ holds
ex b₃ being Element of a₁ st
( b₃ in a₂ & b₁ <= b₃ & b₂ <= b₃ );
attr a₂ is filtered means :Def2: :: WAYBEL_0:def 2
for b₁, b₂ being Element of a₁ st b₁ in a₂ & b₂ in a₂ holds
ex b₃ being Element of a₁ st
( b₃ in a₂ & b₃ <= b₁ & b₃ <= b₂ );

end;

:: deftheorem Def1 defines directed WAYBEL_0:def 1 :

:: deftheorem Def2 defines filtered WAYBEL_0:def 2 :

theorem Th1: :: WAYBEL_0:1

for b₁ being non empty transitive RelStr
for b₂ being Subset of b₁ holds
( ( not b₂ is empty & b₂ is directed ) iff for b₃ being finite Subset of b₂ ex b₄ being Element of b₁ st
( b₄ in b₂ & b₄ is_>=_than b₃ ) )

proof end;

theorem Th2: :: WAYBEL_0:2

for b₁ being non empty transitive RelStr
for b₂ being Subset of b₁ holds
( ( not b₂ is empty & b₂ is filtered ) iff for b₃ being finite Subset of b₂ ex b₄ being Element of b₁ st
( b₄ in b₂ & b₄ is_<=_than b₃ ) )

proof end;

registration

let c₁ be RelStr ;
cluster {} a₁ -> directed filtered ;
coherence

proof end;

end;

registration

let c₁ be RelStr ;
cluster directed filtered Element of bool the carrier of a₁;
existence

proof end;

end;

theorem Th3: :: WAYBEL_0:3

for b₁, b₂ being RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ & b₃ is directed holds
b₄ is directed

proof end;

theorem Th4: :: WAYBEL_0:4

proof end;

theorem Th5: :: WAYBEL_0:5

for b₁ being non empty reflexive RelStr
for b₂ being Element of b₁ holds
( {b₂} is directed & {b₂} is filtered )

proof end;

registration

let c₁ be non empty reflexive RelStr ;
cluster non empty finite directed filtered Element of bool the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be with_suprema RelStr ;
cluster [#] a₁ -> directed ;
coherence

proof end;

end;

registration

let c₁ be non empty upper-bounded RelStr ;
cluster [#] a₁ -> directed ;
coherence

proof end;

end;

registration

let c₁ be with_infima RelStr ;
cluster [#] a₁ -> filtered ;
coherence

proof end;

end;

registration

let c₁ be non empty lower-bounded RelStr ;
cluster [#] a₁ -> filtered ;
coherence

proof end;

end;

definition

let c₁ be non empty RelStr ;
let c₂ be SubRelStr of c₁;
attr a₂ is filtered-infs-inheriting means :Def3: :: WAYBEL_0:def 3
for b₁ being filtered Subset of a₂ st b₁ <> {} & ex_inf_of b₁,a₁ holds
"/\" b₁,a₁ in the carrier of a₂;
attr a₂ is directed-sups-inheriting means :Def4: :: WAYBEL_0:def 4
for b₁ being directed Subset of a₂ st b₁ <> {} & ex_sup_of b₁,a₁ holds
"\/" b₁,a₁ in the carrier of a₂;

end;

:: deftheorem Def3 defines filtered-infs-inheriting WAYBEL_0:def 3 :

:: deftheorem Def4 defines directed-sups-inheriting WAYBEL_0:def 4 :

registration

let c₁ be non empty RelStr ;
cluster infs-inheriting -> filtered-infs-inheriting SubRelStr of a₁;
coherence

proof end;

cluster sups-inheriting -> directed-sups-inheriting SubRelStr of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty RelStr ;
cluster non empty strict full infs-inheriting sups-inheriting filtered-infs-inheriting directed-sups-inheriting SubRelStr of a₁;
existence

proof end;

end;

theorem Th6: :: WAYBEL_0:6

for b₁ being non empty transitive RelStr
for b₂ being non empty full filtered-infs-inheriting SubRelStr of b₁
for b₃ being filtered Subset of b₂ st b₃ <> {} & ex_inf_of b₃,b₁ holds
( ex_inf_of b₃,b₂ & "/\" b₃,b₂ = "/\" b₃,b₁ )

proof end;

theorem Th7: :: WAYBEL_0:7

for b₁ being non empty transitive RelStr
for b₂ being non empty full directed-sups-inheriting SubRelStr of b₁
for b₃ being directed Subset of b₂ st b₃ <> {} & ex_sup_of b₃,b₁ holds
( ex_sup_of b₃,b₂ & "\/" b₃,b₂ = "\/" b₃,b₁ )

proof end;

definition

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

proof end;

end;

definition

let c₁, c₂ be RelStr ;
let c₃ be Function of c₁,c₂;
attr a₃ is antitone means :: WAYBEL_0:def 5
for b₁, b₂ being Element of a₁ st b₁ <= b₂ holds
for b₃, b₄ being Element of a₂ st b₃ = a₃ . b₁ & b₄ = a₃ . b₂ holds
b₃ >= b₄;

end;

:: deftheorem Def5 defines antitone WAYBEL_0:def 5 :

definition

let c₁ be 1-sorted ;
attr a₂ is strict;
struct NetStr of c₁ -> RelStr ;
aggr NetStr(# carrier, InternalRel, mapping #) -> NetStr of a₁;
sel mapping c₂ -> Function of the carrier of a₂,the carrier of a₁;

end;

registration

let c₁ be 1-sorted ;
let c₂ be non empty set ;
let c₃ be Relation of c₂;
let c₄ be Function of c₂,the carrier of c₁;
cluster NetStr(# a₂,a₃,a₄ #) -> non empty ;
coherence

proof end;

end;

definition

let c₁ be RelStr ;
attr a₁ is directed means :Def6: :: WAYBEL_0:def 6
[#] a₁ is directed;

end;

:: deftheorem Def6 defines directed WAYBEL_0:def 6 :

registration

let c₁ be 1-sorted ;
cluster non empty reflexive transitive antisymmetric strict directed NetStr of a₁;
existence

proof end;

end;

definition

let c₁ be 1-sorted ;
mode prenet of a₁ is non empty directed NetStr of a₁;

end;

definition

let c₁ be 1-sorted ;
mode net of a₁ is transitive prenet of a₁;

end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be non empty NetStr of c₁;
func netmap c₂,c₁ -> Function of a₂,a₁ equals :: WAYBEL_0:def 7
the mapping of a₂;
coherence ;
let c₃ be Element of c₂;
func c₂ . c₃ -> Element of a₁ equals :: WAYBEL_0:def 8
the mapping of a₂ . a₃;
correctness ;

end;

:: deftheorem Def7 defines netmap WAYBEL_0:def 7 :

:: deftheorem Def8 defines . WAYBEL_0:def 8 :

definition

let c₁ be non empty RelStr ;
let c₂ be non empty NetStr of c₁;
attr a₂ is monotone means :: WAYBEL_0:def 9
netmap a₂,a₁ is monotone;
attr a₂ is antitone means :: WAYBEL_0:def 10
netmap a₂,a₁ is antitone;

end;

:: deftheorem Def9 defines monotone WAYBEL_0:def 9 :

:: deftheorem Def10 defines antitone WAYBEL_0:def 10 :

definition

let c₁ be non empty 1-sorted ;
let c₂ be non empty NetStr of c₁;
let c₃ be set ;
pred c₂ is_eventually_in c₃ means :Def11: :: WAYBEL_0:def 11
ex b₁ being Element of a₂ st
for b₂ being Element of a₂ st b₁ <= b₂ holds
a₂ . b₂ in a₃;
pred c₂ is_often_in c₃ means :: WAYBEL_0:def 12
for b₁ being Element of a₂ ex b₂ being Element of a₂ st
( b₁ <= b₂ & a₂ . b₂ in a₃ );

end;

:: deftheorem Def11 defines is_eventually_in WAYBEL_0:def 11 :

:: deftheorem Def12 defines is_often_in WAYBEL_0:def 12 :

theorem Th8: :: WAYBEL_0:8

for b₁ being non empty 1-sorted
for b₂ being non empty NetStr of b₁
for b₃, b₄ being set st b₃ c= b₄ holds
( ( b₂ is_eventually_in b₃ implies b₂ is_eventually_in b₄ ) & ( b₂ is_often_in b₃ implies b₂ is_often_in b₄ ) )

proof end;

theorem Th9: :: WAYBEL_0:9

for b₁ being non empty 1-sorted
for b₂ being non empty NetStr of b₁
for b₃ being set holds
( b₂ is_eventually_in b₃ iff not b₂ is_often_in the carrier of b₁ \ b₃ )

proof end;

theorem Th10: :: WAYBEL_0:10

for b₁ being non empty 1-sorted
for b₂ being non empty NetStr of b₁
for b₃ being set holds
( b₂ is_often_in b₃ iff not b₂ is_eventually_in the carrier of b₁ \ b₃ )

proof end;

scheme :: WAYBEL_0:sch 1
s1{ F₁() -> non empty RelStr , F₂() -> non empty NetStr of F₁(), P₁[ set ] } :

( F₂() is_eventually_in { (F₂() . b₁) where B is Element of F₂() : P₁[F₂() . b₁] } iff ex b₁ being Element of F₂() st
for b₂ being Element of F₂() st b₁ <= b₂ holds
P₁[F₂() . b₂] )

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be non empty NetStr of c₁;
attr a₂ is eventually-directed means :Def13: :: WAYBEL_0:def 13
for b₁ being Element of a₂ holds a₂ is_eventually_in { (a₂ . b₂) where B is Element of a₂ : a₂ . b₁ <= a₂ . b₂ } ;
attr a₂ is eventually-filtered means :Def14: :: WAYBEL_0:def 14
for b₁ being Element of a₂ holds a₂ is_eventually_in { (a₂ . b₂) where B is Element of a₂ : a₂ . b₁ >= a₂ . b₂ } ;

end;

:: deftheorem Def13 defines eventually-directed WAYBEL_0:def 13 :

:: deftheorem Def14 defines eventually-filtered WAYBEL_0:def 14 :

theorem Th11: :: WAYBEL_0:11

for b₁ being non empty RelStr
for b₂ being non empty NetStr of b₁ holds
( b₂ is eventually-directed iff for b₃ being Element of b₂ ex b₄ being Element of b₂ st
for b₅ being Element of b₂ st b₄ <= b₅ holds
b₂ . b₃ <= b₂ . b₅ )

proof end;

theorem Th12: :: WAYBEL_0:12

for b₁ being non empty RelStr
for b₂ being non empty NetStr of b₁ holds
( b₂ is eventually-filtered iff for b₃ being Element of b₂ ex b₄ being Element of b₂ st
for b₅ being Element of b₂ st b₄ <= b₅ holds
b₂ . b₃ >= b₂ . b₅ )

proof end;

registration

let c₁ be non empty RelStr ;
cluster monotone -> eventually-directed NetStr of a₁;
coherence

proof end;

cluster antitone -> eventually-filtered NetStr of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty reflexive RelStr ;
cluster strict monotone antitone eventually-directed eventually-filtered NetStr of a₁;
existence

proof end;

end;

definition

let c₁ be RelStr ;
let c₂ be Subset of c₁;
func downarrow c₂ -> Subset of a₁ means :Def15: :: WAYBEL_0:def 15
for b₁ being Element of a₁ holds
( b₁ in a₃ iff ex b₂ being Element of a₁ st
( b₂ >= b₁ & b₂ in a₂ ) );
existence

proof end;

uniqueness

proof end;

func uparrow c₂ -> Subset of a₁ means :Def16: :: WAYBEL_0:def 16
for b₁ being Element of a₁ holds
( b₁ in a₃ iff ex b₂ being Element of a₁ st
( b₂ <= b₁ & b₂ in a₂ ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def15 defines downarrow WAYBEL_0:def 15 :

:: deftheorem Def16 defines uparrow WAYBEL_0:def 16 :

theorem Th13: :: WAYBEL_0:13

proof end;

theorem Th14: :: WAYBEL_0:14

for b₁ being non empty RelStr
for b₂ being Subset of b₁ holds downarrow b₂ = { b₃ where B is Element of b₁ : ex b₁ being Element of b₁ st
( b₃ <= b₄ & b₄ in b₂ ) }

proof end;

theorem Th15: :: WAYBEL_0:15

for b₁ being non empty RelStr
for b₂ being Subset of b₁ holds uparrow b₂ = { b₃ where B is Element of b₁ : ex b₁ being Element of b₁ st
( b₃ >= b₄ & b₄ in b₂ ) }

proof end;

registration

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

proof end;

cluster uparrow a₂ -> non empty ;
coherence

proof end;

end;

theorem Th16: :: WAYBEL_0:16

for b₁ being reflexive RelStr
for b₂ being Subset of b₁ holds
( b₂ c= downarrow b₂ & b₂ c= uparrow b₂ )

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
func downarrow c₂ -> Subset of a₁ equals :: WAYBEL_0:def 17
downarrow {a₂};
correctness ;
func uparrow c₂ -> Subset of a₁ equals :: WAYBEL_0:def 18
uparrow {a₂};
correctness ;

end;

:: deftheorem Def17 defines downarrow WAYBEL_0:def 17 :

:: deftheorem Def18 defines uparrow WAYBEL_0:def 18 :

theorem Th17: :: WAYBEL_0:17

for b₁ being non empty RelStr
for b₂, b₃ being Element of b₁ holds
( b₃ in downarrow b₂ iff b₃ <= b₂ )

proof end;

theorem Th18: :: WAYBEL_0:18

for b₁ being non empty RelStr
for b₂, b₃ being Element of b₁ holds
( b₃ in uparrow b₂ iff b₂ <= b₃ )

proof end;

theorem Th19: :: WAYBEL_0:19

for b₁ being non empty reflexive antisymmetric RelStr
for b₂, b₃ being Element of b₁ st downarrow b₂ = downarrow b₃ holds
b₂ = b₃

proof end;

theorem Th20: :: WAYBEL_0:20

for b₁ being non empty reflexive antisymmetric RelStr
for b₂, b₃ being Element of b₁ st uparrow b₂ = uparrow b₃ holds
b₂ = b₃

proof end;

theorem Th21: :: WAYBEL_0:21

for b₁ being non empty transitive RelStr
for b₂, b₃ being Element of b₁ st b₂ <= b₃ holds
downarrow b₂ c= downarrow b₃

proof end;

theorem Th22: :: WAYBEL_0:22

for b₁ being non empty transitive RelStr
for b₂, b₃ being Element of b₁ st b₂ <= b₃ holds
uparrow b₃ c= uparrow b₂

proof end;

registration

let c₁ be non empty reflexive RelStr ;
let c₂ be Element of c₁;
cluster downarrow a₂ -> non empty directed ;
coherence

proof end;

cluster uparrow a₂ -> non empty filtered ;
coherence

proof end;

end;

definition

let c₁ be RelStr ;
let c₂ be Subset of c₁;
attr a₂ is lower means :Def19: :: WAYBEL_0:def 19
for b₁, b₂ being Element of a₁ st b₁ in a₂ & b₂ <= b₁ holds
b₂ in a₂;
attr a₂ is upper means :Def20: :: WAYBEL_0:def 20
for b₁, b₂ being Element of a₁ st b₁ in a₂ & b₁ <= b₂ holds
b₂ in a₂;

end;

:: deftheorem Def19 defines lower WAYBEL_0:def 19 :

:: deftheorem Def20 defines upper WAYBEL_0:def 20 :

registration

let c₁ be RelStr ;
cluster lower upper Element of bool the carrier of a₁;
existence

proof end;

end;

theorem Th23: :: WAYBEL_0:23

for b₁ being RelStr
for b₂ being Subset of b₁ holds
( b₂ is lower iff downarrow b₂ c= b₂ )

proof end;

theorem Th24: :: WAYBEL_0:24

for b₁ being RelStr
for b₂ being Subset of b₁ holds
( b₂ is upper iff uparrow b₂ c= b₂ )

proof end;

theorem Th25: :: WAYBEL_0:25

proof end;

theorem Th26: :: WAYBEL_0:26

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
union b₂ is lower Subset of b₁

proof end;

theorem Th27: :: WAYBEL_0:27

for b₁ being RelStr
for b₂, b₃ being Subset of b₁ st b₂ is lower & b₃ is lower holds
( b₂ /\ b₃ is lower & b₂ \/ b₃ is lower )

proof end;

theorem Th28: :: WAYBEL_0:28

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
union b₂ is upper Subset of b₁

proof end;

theorem Th29: :: WAYBEL_0:29

for b₁ being RelStr
for b₂, b₃ being Subset of b₁ st b₂ is upper & b₃ is upper holds
( b₂ /\ b₃ is upper & b₂ \/ b₃ is upper )

proof end;

registration

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

proof end;

cluster uparrow a₂ -> upper ;
coherence

proof end;

end;

registration

let c₁ be non empty transitive RelStr ;
let c₂ be Element of c₁;
cluster downarrow a₂ -> lower ;
coherence ;
cluster uparrow a₂ -> upper ;
coherence ;

end;

registration

let c₁ be non empty RelStr ;
cluster [#] a₁ -> lower upper ;
coherence

proof end;

end;

registration

let c₁ be non empty RelStr ;
cluster non empty lower upper Element of bool the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be non empty reflexive transitive RelStr ;
cluster non empty directed lower Element of bool the carrier of a₁;
existence

proof end;

cluster non empty filtered upper Element of bool the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be with_suprema with_infima Poset;
cluster non empty directed filtered lower upper Element of bool the carrier of a₁;
existence

proof end;

end;

theorem Th30: :: WAYBEL_0:30

for b₁ being non empty reflexive transitive RelStr
for b₂ being Subset of b₁ holds
( b₂ is directed iff downarrow b₂ is directed )

proof end;

registration

let c₁ be non empty reflexive transitive RelStr ;
let c₂ be directed Subset of c₁;
cluster downarrow a₂ -> directed lower ;
coherence by Th30;

end;

theorem Th31: :: WAYBEL_0:31

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

proof end;

theorem Th32: :: WAYBEL_0:32

for b₁ being non empty reflexive transitive RelStr
for b₂ being Subset of b₁ holds
( ex_sup_of b₂,b₁ iff ex_sup_of downarrow b₂,b₁ )

proof end;

theorem Th33: :: WAYBEL_0:33

for b₁ being non empty reflexive transitive RelStr
for b₂ being Subset of b₁ st ex_sup_of b₂,b₁ holds
sup b₂ = sup (downarrow b₂)

proof end;

theorem Th34: :: WAYBEL_0:34

for b₁ being non empty Poset
for b₂ being Element of b₁ holds
( ex_sup_of downarrow b₂,b₁ & sup (downarrow b₂) = b₂ )

proof end;

theorem Th35: :: WAYBEL_0:35

for b₁ being non empty reflexive transitive RelStr
for b₂ being Subset of b₁ holds
( b₂ is filtered iff uparrow b₂ is filtered )

proof end;

registration

let c₁ be non empty reflexive transitive RelStr ;
let c₂ be filtered Subset of c₁;
cluster uparrow a₂ -> filtered upper ;
coherence by Th35;

end;

theorem Th36: :: WAYBEL_0:36

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

proof end;

theorem Th37: :: WAYBEL_0:37

for b₁ being non empty reflexive transitive RelStr
for b₂ being Subset of b₁ holds
( ex_inf_of b₂,b₁ iff ex_inf_of uparrow b₂,b₁ )

proof end;

theorem Th38: :: WAYBEL_0:38

for b₁ being non empty reflexive transitive RelStr
for b₂ being Subset of b₁ st ex_inf_of b₂,b₁ holds
inf b₂ = inf (uparrow b₂)

proof end;

theorem Th39: :: WAYBEL_0:39

for b₁ being non empty Poset
for b₂ being Element of b₁ holds
( ex_inf_of uparrow b₂,b₁ & inf (uparrow b₂) = b₂ )

proof end;

definition

let c₁ be non empty reflexive transitive RelStr ;
mode Ideal of a₁ is non empty directed lower Subset of a₁;
mode Filter of a₁ is non empty filtered upper Subset of a₁;

end;

theorem Th40: :: WAYBEL_0:40

for b₁ being antisymmetric with_suprema RelStr
for b₂ being lower Subset of b₁ holds
( b₂ is directed iff for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₄ in b₂ holds
b₃ "\/" b₄ in b₂ )

proof end;

theorem Th41: :: WAYBEL_0:41

for b₁ being antisymmetric with_infima RelStr
for b₂ being upper Subset of b₁ holds
( b₂ is filtered iff for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₄ in b₂ holds
b₃ "/\" b₄ in b₂ )

proof end;

theorem Th42: :: WAYBEL_0:42

for b₁ being with_suprema Poset
for b₂ being non empty lower Subset of b₁ holds
( b₂ is directed iff for b₃ being finite Subset of b₂ st b₃ <> {} holds
"\/" b₃,b₁ in b₂ )

proof end;

theorem Th43: :: WAYBEL_0:43

for b₁ being with_infima Poset
for b₂ being non empty upper Subset of b₁ holds
( b₂ is filtered iff for b₃ being finite Subset of b₂ st b₃ <> {} holds
"/\" b₃,b₁ in b₂ )

proof end;

theorem Th44: :: WAYBEL_0:44

for b₁ being non empty antisymmetric RelStr st ( b₁ is with_suprema or b₁ is with_infima ) holds
for b₂, b₃ being Subset of b₁ st b₂ is lower & b₂ is directed & b₃ is lower & b₃ is directed holds
b₂ /\ b₃ is directed

proof end;

theorem Th45: :: WAYBEL_0:45

for b₁ being non empty antisymmetric RelStr st ( b₁ is with_suprema or b₁ is with_infima ) holds
for b₂, b₃ being Subset of b₁ st b₂ is upper & b₂ is filtered & b₃ is upper & b₃ is filtered holds
b₂ /\ b₃ is filtered

proof end;

theorem Th46: :: WAYBEL_0:46

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 directed ) & ( for b₃, b₄ being Subset of b₁ st b₃ in b₂ & b₄ in b₂ holds
ex b₅ being Subset of b₁ st
( b₅ in b₂ & b₃ \/ b₄ c= b₅ ) ) holds
for b₃ being Subset of b₁ st b₃ = union b₂ holds
b₃ is directed

proof end;

theorem Th47: :: WAYBEL_0:47

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 filtered ) & ( for b₃, b₄ being Subset of b₁ st b₃ in b₂ & b₄ in b₂ holds
ex b₅ being Subset of b₁ st
( b₅ in b₂ & b₃ \/ b₄ c= b₅ ) ) holds
for b₃ being Subset of b₁ st b₃ = union b₂ holds
b₃ is filtered

proof end;

definition

let c₁ be non empty reflexive transitive RelStr ;
let c₂ be Ideal of c₁;
attr a₂ is principal means :: WAYBEL_0:def 21
ex b₁ being Element of a₁ st
( b₁ in a₂ & b₁ is_>=_than a₂ );

end;

:: deftheorem Def21 defines principal WAYBEL_0:def 21 :

definition

let c₁ be non empty reflexive transitive RelStr ;
let c₂ be Filter of c₁;
attr a₂ is principal means :: WAYBEL_0:def 22
ex b₁ being Element of a₁ st
( b₁ in a₂ & b₁ is_<=_than a₂ );

end;

:: deftheorem Def22 defines principal WAYBEL_0:def 22 :

theorem Th48: :: WAYBEL_0:48

for b₁ being non empty reflexive transitive RelStr
for b₂ being Ideal of b₁ holds
( b₂ is principal iff ex b₃ being Element of b₁ st b₂ = downarrow b₃ )

proof end;

theorem Th49: :: WAYBEL_0:49

for b₁ being non empty reflexive transitive RelStr
for b₂ being Filter of b₁ holds
( b₂ is principal iff ex b₃ being Element of b₁ st b₂ = uparrow b₃ )

proof end;

definition

let c₁ be non empty reflexive transitive RelStr ;
func Ids c₁ -> set equals :: WAYBEL_0:def 23
{ b₁ where B is Ideal of a₁ : verum } ;
correctness ;
func Filt c₁ -> set equals :: WAYBEL_0:def 24
{ b₁ where B is Filter of a₁ : verum } ;
correctness ;

end;

:: deftheorem Def23 defines Ids WAYBEL_0:def 23 :

:: deftheorem Def24 defines Filt WAYBEL_0:def 24 :

definition

let c₁ be non empty reflexive transitive RelStr ;
func Ids_0 c₁ -> set equals :: WAYBEL_0:def 25
(Ids a₁) \/ {{} };
correctness ;
func Filt_0 c₁ -> set equals :: WAYBEL_0:def 26
(Filt a₁) \/ {{} };
correctness ;

end;

:: deftheorem Def25 defines Ids_0 WAYBEL_0:def 25 :

:: deftheorem Def26 defines Filt_0 WAYBEL_0:def 26 :

definition

let c₁ be non empty RelStr ;
let c₂ be Subset of c₁;
set c₃ = { ("\/" b₁,c₁) where B is finite Subset of c₂ : ex_sup_of b₁,c₁ } ;
E43: { ("\/" b₁,c₁) where B is finite Subset of c₂ : ex_sup_of b₁,c₁ } c= the carrier of c₁

proof end;

func finsups c₂ -> Subset of a₁ equals :: WAYBEL_0:def 27
{ ("\/" b₁,a₁) where B is finite Subset of a₂ : ex_sup_of b₁,a₁ } ;
correctness by E43;
set c₄ = { ("/\" b₁,c₁) where B is finite Subset of c₂ : ex_inf_of b₁,c₁ } ;
E44: { ("/\" b₁,c₁) where B is finite Subset of c₂ : ex_inf_of b₁,c₁ } c= the carrier of c₁

proof end;

func fininfs c₂ -> Subset of a₁ equals :: WAYBEL_0:def 28
{ ("/\" b₁,a₁) where B is finite Subset of a₂ : ex_inf_of b₁,a₁ } ;
correctness by E44;

end;

:: deftheorem Def27 defines finsups WAYBEL_0:def 27 :

:: deftheorem Def28 defines fininfs WAYBEL_0:def 28 :

registration

let c₁ be non empty antisymmetric lower-bounded RelStr ;
let c₂ be Subset of c₁;
cluster finsups a₂ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be non empty antisymmetric upper-bounded RelStr ;
let c₂ be Subset of c₁;
cluster fininfs a₂ -> non empty ;
coherence

proof end;

end;

registration

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

proof end;

cluster fininfs a₂ -> non empty ;
coherence

proof end;

end;

theorem Th50: :: WAYBEL_0:50

for b₁ being non empty reflexive antisymmetric RelStr
for b₂ being Subset of b₁ holds
( b₂ c= finsups b₂ & b₂ c= fininfs b₂ )

proof end;

theorem Th51: :: WAYBEL_0:51

for b₁ being non empty transitive RelStr
for b₂, b₃ being Subset of b₁ st ( for b₄ being finite Subset of b₂ st b₄ <> {} holds
ex_sup_of b₄,b₁ ) & ( for b₄ being Element of b₁ st b₄ in b₃ holds
ex b₅ being finite Subset of b₂ st
( ex_sup_of b₅,b₁ & b₄ = "\/" b₅,b₁ ) ) & ( for b₄ being finite Subset of b₂ st b₄ <> {} holds
"\/" b₄,b₁ in b₃ ) holds
b₃ is directed

proof end;

registration

let c₁ be with_suprema Poset;
let c₂ be Subset of c₁;
cluster finsups a₂ -> directed ;
coherence

proof end;

end;

theorem Th52: :: WAYBEL_0:52

for b₁ being non empty reflexive transitive RelStr
for b₂, b₃ being Subset of b₁ st ( for b₄ being finite Subset of b₂ st b₄ <> {} holds
ex_sup_of b₄,b₁ ) & ( for b₄ being Element of b₁ st b₄ in b₃ holds
ex b₅ being finite Subset of b₂ st
( ex_sup_of b₅,b₁ & b₄ = "\/" b₅,b₁ ) ) & ( for b₄ being finite Subset of b₂ st b₄ <> {} holds
"\/" b₄,b₁ in b₃ ) holds
for b₄ being Element of b₁ holds
( b₄ is_>=_than b₂ iff b₄ is_>=_than b₃ )

proof end;

theorem Th53: :: WAYBEL_0:53

proof end;

theorem Th54: :: WAYBEL_0:54

proof end;

theorem Th55: :: WAYBEL_0:55

for b₁ being with_suprema Poset
for b₂ being Subset of b₁ st ( ex_sup_of b₂,b₁ or b₁ is complete ) holds
sup b₂ = sup (finsups b₂)

proof end;

theorem Th56: :: WAYBEL_0:56

for b₁ being non empty transitive RelStr
for b₂, b₃ being Subset of b₁ st ( for b₄ being finite Subset of b₂ st b₄ <> {} holds
ex_inf_of b₄,b₁ ) & ( for b₄ being Element of b₁ st b₄ in b₃ holds
ex b₅ being finite Subset of b₂ st
( ex_inf_of b₅,b₁ & b₄ = "/\" b₅,b₁ ) ) & ( for b₄ being finite Subset of b₂ st b₄ <> {} holds
"/\" b₄,b₁ in b₃ ) holds
b₃ is filtered

proof end;

registration

let c₁ be with_infima Poset;
let c₂ be Subset of c₁;
cluster fininfs a₂ -> filtered ;
coherence

proof end;

end;

theorem Th57: :: WAYBEL_0:57

for b₁ being non empty reflexive transitive RelStr
for b₂, b₃ being Subset of b₁ st ( for b₄ being finite Subset of b₂ st b₄ <> {} holds
ex_inf_of b₄,b₁ ) & ( for b₄ being Element of b₁ st b₄ in b₃ holds
ex b₅ being finite Subset of b₂ st
( ex_inf_of b₅,b₁ & b₄ = "/\" b₅,b₁ ) ) & ( for b₄ being finite Subset of b₂ st b₄ <> {} holds
"/\" b₄,b₁ in b₃ ) holds
for b₄ being Element of b₁ holds
( b₄ is_<=_than b₂ iff b₄ is_<=_than b₃ )

proof end;

theorem Th58: :: WAYBEL_0:58

proof end;

theorem Th59: :: WAYBEL_0:59

proof end;

theorem Th60: :: WAYBEL_0:60

for b₁ being with_infima Poset
for b₂ being Subset of b₁ st ( ex_inf_of b₂,b₁ or b₁ is complete ) holds
inf b₂ = inf (fininfs b₂)

proof end;

theorem Th61: :: WAYBEL_0:61

for b₁ being with_suprema Poset
for b₂ being Subset of b₁ holds
( b₂ c= downarrow (finsups b₂) & ( for b₃ being Ideal of b₁ st b₂ c= b₃ holds
downarrow (finsups b₂) c= b₃ ) )

proof end;

theorem Th62: :: WAYBEL_0:62

for b₁ being with_infima Poset
for b₂ being Subset of b₁ holds
( b₂ c= uparrow (fininfs b₂) & ( for b₃ being Filter of b₁ st b₂ c= b₃ holds
uparrow (fininfs b₂) c= b₃ ) )

proof end;

definition

let c₁ be non empty RelStr ;
attr a₁ is connected means :Def29: :: WAYBEL_0:def 29
for b₁, b₂ being Element of a₁ holds
( b₁ <= b₂ or b₂ <= b₁ );

end;

:: deftheorem Def29 defines connected WAYBEL_0:def 29 :

registration

cluster non empty reflexive trivial -> non empty reflexive connected RelStr ;
coherence

proof end;

end;

registration

cluster non empty connected RelStr ;
existence

proof end;

end;

definition

mode Chain is non empty connected Poset;

end;

registration

let c₁ be Chain;
cluster a₁ ~ -> connected ;
coherence

proof end;

end;

definition

mode Semilattice is with_infima Poset;
mode sup-Semilattice is with_suprema Poset;
mode LATTICE is with_suprema with_infima Poset;

end;

theorem Th63: :: WAYBEL_0:63

for b₁ being Semilattice
for b₂ being non empty upper Subset of b₁ holds
( b₂ is Filter of b₁ iff subrelstr b₂ is meet-inheriting )

proof end;

theorem Th64: :: WAYBEL_0:64

for b₁ being sup-Semilattice
for b₂ being non empty lower Subset of b₁ holds
( b₂ is Ideal of b₁ iff subrelstr b₂ is join-inheriting )

proof end;

definition

let c₁, c₂ be non empty RelStr ;
let c₃ be Function of c₁,c₂;
let c₄ be Subset of c₁;
pred c₃ preserves_inf_of c₄ means :Def30: :: WAYBEL_0:def 30
( ex_inf_of a₄,a₁ implies ( ex_inf_of a₃ .: a₄,a₂ & inf (a₃ .: a₄) = a₃ . (inf a₄) ) );
pred c₃ preserves_sup_of c₄ means :Def31: :: WAYBEL_0:def 31
( ex_sup_of a₄,a₁ implies ( ex_sup_of a₃ .: a₄,a₂ & sup (a₃ .: a₄) = a₃ . (sup a₄) ) );

end;

:: deftheorem Def30 defines preserves_inf_of WAYBEL_0:def 30 :

:: deftheorem Def31 defines preserves_sup_of WAYBEL_0:def 31 :

theorem Th65: :: WAYBEL_0:65

for b₁, b₂, b₃, b₄ being non empty RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₃,the InternalRel of b₃ #) & RelStr(# the carrier of b₂,the InternalRel of b₂ #) = RelStr(# the carrier of b₄,the InternalRel of b₄ #) holds
for b₅ being Function of b₁,b₂
for b₆ being Function of b₃,b₄ st b₅ = b₆ holds
for b₇ being Subset of b₁
for b₈ being Subset of b₃ st b₇ = b₈ holds
( ( b₅ preserves_sup_of b₇ implies b₆ preserves_sup_of b₈ ) & ( b₅ preserves_inf_of b₇ implies b₆ preserves_inf_of b₈ ) )

proof end;

definition

let c₁, c₂ be non empty RelStr ;
let c₃ be Function of c₁,c₂;
attr a₃ is infs-preserving means :: WAYBEL_0:def 32
for b₁ being Subset of a₁ holds a₃ preserves_inf_of b₁;
attr a₃ is sups-preserving means :: WAYBEL_0:def 33
for b₁ being Subset of a₁ holds a₃ preserves_sup_of b₁;
attr a₃ is meet-preserving means :: WAYBEL_0:def 34
for b₁, b₂ being Element of a₁ holds a₃ preserves_inf_of {b₁,b₂};
attr a₃ is join-preserving means :: WAYBEL_0:def 35
for b₁, b₂ being Element of a₁ holds a₃ preserves_sup_of {b₁,b₂};
attr a₃ is filtered-infs-preserving means :: WAYBEL_0:def 36
for b₁ being Subset of a₁ st not b₁ is empty & b₁ is filtered holds
a₃ preserves_inf_of b₁;
attr a₃ is directed-sups-preserving means :: WAYBEL_0:def 37
for b₁ being Subset of a₁ st not b₁ is empty & b₁ is directed holds
a₃ preserves_sup_of b₁;

end;

:: deftheorem Def32 defines infs-preserving WAYBEL_0:def 32 :

:: deftheorem Def33 defines sups-preserving WAYBEL_0:def 33 :

:: deftheorem Def34 defines meet-preserving WAYBEL_0:def 34 :

:: deftheorem Def35 defines join-preserving WAYBEL_0:def 35 :

:: deftheorem Def36 defines filtered-infs-preserving WAYBEL_0:def 36 :

:: deftheorem Def37 defines directed-sups-preserving WAYBEL_0:def 37 :

registration

let c₁, c₂ be non empty RelStr ;
cluster infs-preserving -> meet-preserving filtered-infs-preserving Relation of the carrier of a₁,the carrier of a₂;
coherence

proof end;

cluster sups-preserving -> join-preserving directed-sups-preserving Relation of the carrier of a₁,the carrier of a₂;
coherence

proof end;

end;

definition

let c₁, c₂ be RelStr ;
let c₃ be Function of c₁,c₂;
attr a₃ is isomorphic means :Def38: :: WAYBEL_0:def 38
( a₃ is one-to-one & a₃ is monotone & ex b₁ being Function of a₂,a₁ st
( b₁ = a₃ " & b₁ is monotone ) ) if ( not a₁ is empty & not a₂ is empty )
otherwise ( a₁ is empty & a₂ is empty );
correctness ;

end;

:: deftheorem Def38 defines isomorphic WAYBEL_0:def 38 :

theorem Th66: :: WAYBEL_0:66

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂ holds
( b₃ is isomorphic iff ( b₃ is one-to-one & rng b₃ = the carrier of b₂ & ( for b₄, b₅ being Element of b₁ holds
( b₄ <= b₅ iff b₃ . b₄ <= b₃ . b₅ ) ) ) )

proof end;

registration

let c₁, c₂ be non empty RelStr ;
cluster isomorphic -> one-to-one monotone Relation of the carrier of a₁,the carrier of a₂;
coherence by Def38;

end;

theorem Th67: :: WAYBEL_0:67

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂ st b₃ is isomorphic holds
( b₃ " is Function of b₂,b₁ & rng (b₃ " ) = the carrier of b₁ )

proof end;

theorem Th68: :: WAYBEL_0:68

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂ st b₃ is isomorphic holds
for b₄ being Function of b₂,b₁ st b₄ = b₃ " holds
b₄ is isomorphic

proof end;

theorem Th69: :: WAYBEL_0:69

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂ st ( for b₄ being Filter of b₁ holds b₃ preserves_inf_of b₄ ) holds
b₃ is monotone

proof end;

theorem Th70: :: WAYBEL_0:70

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂ st ( for b₄ being Filter of b₁ holds b₃ preserves_inf_of b₄ ) holds
b₃ is filtered-infs-preserving

proof end;

theorem Th71: :: WAYBEL_0:71

for b₁ being Semilattice
for b₂ being non empty Poset
for b₃ being Function of b₁,b₂ st ( for b₄ being finite Subset of b₁ holds b₃ preserves_inf_of b₄ ) & ( for b₄ being non empty filtered Subset of b₁ holds b₃ preserves_inf_of b₄ ) holds
b₃ is infs-preserving

proof end;

theorem Th72: :: WAYBEL_0:72

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂ st ( for b₄ being Ideal of b₁ holds b₃ preserves_sup_of b₄ ) holds
b₃ is monotone

proof end;

theorem Th73: :: WAYBEL_0:73

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂ st ( for b₄ being Ideal of b₁ holds b₃ preserves_sup_of b₄ ) holds
b₃ is directed-sups-preserving

proof end;

theorem Th74: :: WAYBEL_0:74

for b₁ being sup-Semilattice
for b₂ being non empty Poset
for b₃ being Function of b₁,b₂ st ( for b₄ being finite Subset of b₁ holds b₃ preserves_sup_of b₄ ) & ( for b₄ being non empty directed Subset of b₁ holds b₃ preserves_sup_of b₄ ) holds
b₃ is sups-preserving

proof end;

definition

let c₁ be non empty reflexive RelStr ;
attr a₁ is up-complete means :Def39: :: WAYBEL_0:def 39
for b₁ being non empty directed Subset of a₁ ex b₂ being Element of a₁ st
( b₂ is_>=_than b₁ & ( for b₃ being Element of a₁ st b₃ is_>=_than b₁ holds
b₂ <= b₃ ) );

end;

:: deftheorem Def39 defines up-complete WAYBEL_0:def 39 :

registration

cluster reflexive with_suprema up-complete -> reflexive with_suprema upper-bounded RelStr ;
coherence

proof end;

end;

theorem Th75: :: WAYBEL_0:75

for b₁ being non empty reflexive antisymmetric RelStr holds
( b₁ is up-complete iff for b₂ being non empty directed Subset of b₁ holds ex_sup_of b₂,b₁ )

proof end;

definition

let c₁ be non empty reflexive RelStr ;
attr a₁ is /\-complete means :Def40: :: WAYBEL_0:def 40
for b₁ being non empty Subset of a₁ ex b₂ being Element of a₁ st
( b₂ is_<=_than b₁ & ( for b₃ being Element of a₁ st b₃ is_<=_than b₁ holds
b₂ >= b₃ ) );

end;