:: WAYBEL_3 semantic presentation

definition

let c₁ be non empty reflexive RelStr ;
let c₂, c₃ be Element of c₁;
pred c₂ is_way_below c₃ means :Def1: :: WAYBEL_3:def 1
for b₁ being non empty directed Subset of a₁ st a₃ <= sup b₁ holds
ex b₂ being Element of a₁ st
( b₂ in b₁ & a₂ <= b₂ );

end;

:: deftheorem Def1 defines is_way_below WAYBEL_3:def 1 :

notation

let c₁ be non empty reflexive RelStr ;
let c₂, c₃ be Element of c₁;
synonym c₂ << c₃ for c₂ is_way_below c₃;
synonym c₃ >> c₂ for c₂ is_way_below c₃;

end;

definition

let c₁ be non empty reflexive RelStr ;
let c₂ be Element of c₁;
attr a₂ is compact means :Def2: :: WAYBEL_3:def 2
a₂ is_way_below a₂;

end;

:: deftheorem Def2 defines compact WAYBEL_3:def 2 :

notation

let c₁ be non empty reflexive RelStr ;
let c₂ be Element of c₁;
synonym isolated_from_below c₂ for compact c₂;

end;

theorem Th1: :: WAYBEL_3:1

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

proof end;

theorem Th2: :: WAYBEL_3:2

for b₁ being non empty reflexive transitive RelStr
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <= b₃ & b₃ << b₄ & b₄ <= b₅ holds
b₂ << b₅

proof end;

theorem Th3: :: WAYBEL_3:3

for b₁ being non empty Poset st ( b₁ is with_suprema or b₁ is /\-complete ) holds
for b₂, b₃, b₄ being Element of b₁ st b₂ << b₄ & b₃ << b₄ holds
( ex_sup_of {b₂,b₃},b₁ & b₂ "\/" b₃ << b₄ )

proof end;

theorem Th4: :: WAYBEL_3:4

for b₁ being non empty reflexive antisymmetric lower-bounded RelStr
for b₂ being Element of b₁ holds Bottom b₁ << b₂

proof end;

theorem Th5: :: WAYBEL_3:5

for b₁ being non empty Poset
for b₂, b₃, b₄ being Element of b₁ st b₂ << b₃ & b₃ << b₄ holds
b₂ << b₄

proof end;

theorem Th6: :: WAYBEL_3:6

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

proof end;

definition

let c₁ be non empty reflexive RelStr ;
let c₂ be Element of c₁;
E7: { b₁ where B is Element of c₁ : b₁ << c₂ } c= the carrier of c₁

proof end;

func waybelow c₂ -> Subset of a₁ equals :: WAYBEL_3:def 3
{ b₁ where B is Element of a₁ : b₁ << a₂ } ;
correctness by E7;
E8: { b₁ where B is Element of c₁ : b₁ >> c₂ } c= the carrier of c₁

proof end;

func wayabove c₂ -> Subset of a₁ equals :: WAYBEL_3:def 4
{ b₁ where B is Element of a₁ : b₁ >> a₂ } ;
correctness by E8;

end;

:: deftheorem Def3 defines waybelow WAYBEL_3:def 3 :

:: deftheorem Def4 defines wayabove WAYBEL_3:def 4 :

theorem Th7: :: WAYBEL_3:7

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

proof end;

theorem Th8: :: WAYBEL_3:8

for b₁ being non empty reflexive RelStr
for b₂, b₃ being Element of b₁ holds
( b₂ in wayabove b₃ iff b₂ >> b₃ )

proof end;

theorem Th9: :: WAYBEL_3:9

for b₁ being non empty reflexive antisymmetric RelStr
for b₂ being Element of b₁ holds b₂ is_>=_than waybelow b₂

proof end;

theorem Th10: :: WAYBEL_3:10

for b₁ being non empty reflexive antisymmetric RelStr
for b₂ being Element of b₁ holds b₂ is_<=_than wayabove b₂

proof end;

theorem Th11: :: WAYBEL_3:11

for b₁ being non empty reflexive antisymmetric RelStr
for b₂ being Element of b₁ holds
( waybelow b₂ c= downarrow b₂ & wayabove b₂ c= uparrow b₂ )

proof end;

theorem Th12: :: WAYBEL_3:12

for b₁ being non empty reflexive transitive RelStr
for b₂, b₃ being Element of b₁ st b₂ <= b₃ holds
( waybelow b₂ c= waybelow b₃ & wayabove b₃ c= wayabove b₂ )

proof end;

registration

let c₁ be non empty reflexive antisymmetric lower-bounded RelStr ;
let c₂ be Element of c₁;
cluster waybelow a₂ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be non empty reflexive transitive RelStr ;
let c₂ be Element of c₁;
cluster waybelow a₂ -> lower ;
coherence

proof end;

cluster wayabove a₂ -> upper ;
coherence

proof end;

end;

registration

let c₁ be sup-Semilattice;
let c₂ be Element of c₁;
cluster waybelow a₂ -> directed lower ;
coherence

proof end;

end;

registration

let c₁ be non empty /\-complete Poset;
let c₂ be Element of c₁;
cluster waybelow a₂ -> non empty directed lower ;
coherence

proof end;

end;

registration

let c₁ be non empty connected RelStr ;
cluster -> directed filtered Element of K40(the carrier of a₁);
coherence

proof end;

end;

registration

cluster non empty lower-bounded up-complete -> non empty complete RelStr ;
coherence

proof end;

end;

registration

cluster non empty complete RelStr ;
existence

proof end;

end;

theorem Th13: :: WAYBEL_3:13

for b₁ being non empty up-complete Chain
for b₂, b₃ being Element of b₁ st b₂ < b₃ holds
b₂ << b₃

proof end;

theorem Th14: :: WAYBEL_3:14

for b₁ being non empty reflexive antisymmetric RelStr
for b₂, b₃ being Element of b₁ st not b₂ is compact & b₂ << b₃ holds
b₂ < b₃

proof end;

theorem Th15: :: WAYBEL_3:15

for b₁ being non empty reflexive antisymmetric lower-bounded RelStr holds Bottom b₁ is compact

proof end;

theorem Th16: :: WAYBEL_3:16

for b₁ being non empty up-complete Poset
for b₂ being non empty finite directed Subset of b₁ holds sup b₂ in b₂

proof end;

theorem Th17: :: WAYBEL_3:17

for b₁ being non empty up-complete Poset st b₁ is finite holds
for b₂ being Element of b₁ holds b₂ is compact

proof end;

theorem Th18: :: WAYBEL_3:18

for b₁ being complete LATTICE
for b₂, b₃ being Element of b₁ st b₂ << b₃ holds
for b₄ being Subset of b₁ st b₃ <= sup b₄ holds
ex b₅ being finite Subset of b₁ st
( b₅ c= b₄ & b₂ <= sup b₅ )

proof end;

theorem Th19: :: WAYBEL_3:19

for b₁ being complete LATTICE
for b₂, b₃ being Element of b₁ st ( for b₄ being Subset of b₁ st b₃ <= sup b₄ holds
ex b₅ being finite Subset of b₁ st
( b₅ c= b₄ & b₂ <= sup b₅ ) ) holds
b₂ << b₃

proof end;

theorem Th20: :: WAYBEL_3:20

for b₁ being non empty reflexive transitive RelStr
for b₂, b₃ being Element of b₁ st b₂ << b₃ holds
for b₄ being Ideal of b₁ st b₃ <= sup b₄ holds
b₂ in b₄

proof end;

theorem Th21: :: WAYBEL_3:21

for b₁ being non empty up-complete Poset
for b₂, b₃ being Element of b₁ st ( for b₄ being Ideal of b₁ st b₃ <= sup b₄ holds
b₂ in b₄ ) holds
b₂ << b₃

proof end;

theorem Th22: :: WAYBEL_3:22

for b₁ being lower-bounded LATTICE st b₁ is meet-continuous holds
for b₂, b₃ being Element of b₁ holds
( b₂ << b₃ iff for b₄ being Ideal of b₁ st b₃ = sup b₄ holds
b₂ in b₄ )

proof end;

theorem Th23: :: WAYBEL_3:23

for b₁ being complete LATTICE holds
( ( for b₂ being Element of b₁ holds b₂ is compact ) iff for b₂ being non empty Subset of b₁ ex b₃ being Element of b₁ st
( b₃ in b₂ & ( for b₄ being Element of b₁ st b₄ in b₂ holds
not b₃ < b₄ ) ) )

proof end;

definition

let c₁ be non empty reflexive RelStr ;
attr a₁ is satisfying_axiom_of_approximation means :Def5: :: WAYBEL_3:def 5
for b₁ being Element of a₁ holds b₁ = sup (waybelow b₁);

end;

:: deftheorem Def5 defines satisfying_axiom_of_approximation WAYBEL_3:def 5 :

registration

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

proof end;

end;

definition

let c₁ be non empty reflexive RelStr ;
attr a₁ is continuous means :Def6: :: WAYBEL_3:def 6
( ( for b₁ being Element of a₁ holds
( not waybelow b₁ is empty & waybelow b₁ is directed ) ) & a₁ is up-complete & a₁ is satisfying_axiom_of_approximation );

end;

:: deftheorem Def6 defines continuous WAYBEL_3:def 6 :

registration

cluster non empty reflexive continuous -> non empty reflexive up-complete satisfying_axiom_of_approximation RelStr ;
coherence by Def6;
cluster lower-bounded up-complete satisfying_axiom_of_approximation -> lower-bounded continuous RelStr ;
coherence

proof end;

end;

registration

cluster strict complete up-complete satisfying_axiom_of_approximation continuous RelStr ;
existence

proof end;

end;

registration

let c₁ be non empty reflexive continuous RelStr ;
let c₂ be Element of c₁;
cluster waybelow a₂ -> non empty directed ;
coherence by Def6;

end;

theorem Th24: :: WAYBEL_3:24

for b₁ being up-complete Semilattice st ( for b₂ being Element of b₁ holds
( not waybelow b₂ is empty & waybelow b₂ is directed ) ) holds
( b₁ is satisfying_axiom_of_approximation iff for b₂, b₃ being Element of b₁ st not b₂ <= b₃ holds
ex b₄ being Element of b₁ st
( b₄ << b₂ & not b₄ <= b₃ ) )

proof end;

theorem Th25: :: WAYBEL_3:25

for b₁ being continuous LATTICE
for b₂, b₃ being Element of b₁ holds
( b₂ <= b₃ iff waybelow b₂ c= waybelow b₃ )

proof end;

registration

cluster non empty complete -> non empty satisfying_axiom_of_approximation RelStr ;
coherence

proof end;

end;

theorem Th26: :: WAYBEL_3:26

for b₁ being complete LATTICE st ( for b₂ being Element of b₁ holds b₂ is compact ) holds
b₁ is satisfying_axiom_of_approximation

proof end;

definition

let c₁ be Relation;
attr a₁ is non-Empty means :Def7: :: WAYBEL_3:def 7
for b₁ being 1-sorted st b₁ in rng a₁ holds
not b₁ is empty;
attr a₁ is reflexive-yielding means :Def8: :: WAYBEL_3:def 8
for b₁ being RelStr st b₁ in rng a₁ holds
b₁ is reflexive;

end;

:: deftheorem Def7 defines non-Empty WAYBEL_3:def 7 :

:: deftheorem Def8 defines reflexive-yielding WAYBEL_3:def 8 :

registration

let c₁ be set ;
cluster RelStr-yielding non-Empty reflexive-yielding ManySortedSet of a₁;
existence

proof end;

end;

registration

let c₁ be set ;
let c₂ be RelStr-yielding non-Empty ManySortedSet of c₁;
cluster product a₂ -> non empty ;
coherence

proof end;

end;

definition

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

proof end;

end;

registration

let c₁ be set ;
let c₂ be RelStr-yielding non-Empty ManySortedSet of c₁;
cluster product a₂ -> non empty constituted-Functions ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be RelStr-yielding non-Empty ManySortedSet of c₁;
let c₃ be Element of (product c₂);
let c₄ be Element of c₁;
redefine func . as c₃ . c₄ -> Element of (a₂ . a₄);
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be RelStr-yielding non-Empty ManySortedSet of c₁;
let c₃ be Element of c₁;
let c₄ be Subset of (product c₂);
redefine func pi as pi c₄,c₃ -> Subset of (a₂ . a₃);
coherence

proof end;

end;

theorem Th27: :: WAYBEL_3:27

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty ManySortedSet of b₁
for b₃ being Function holds
( b₃ is Element of (product b₂) iff ( dom b₃ = b₁ & ( for b₄ being Element of b₁ holds b₃ . b₄ is Element of (b₂ . b₄) ) ) )

proof end;

theorem Th28: :: WAYBEL_3:28

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty ManySortedSet of b₁
for b₃, b₄ being Element of (product b₂) holds
( b₃ <= b₄ iff for b₅ being Element of b₁ holds b₃ . b₅ <= b₄ . b₅ )

proof end;

definition

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

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of c₁;
cluster product a₂ -> non empty reflexive constituted-Functions ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of c₁;
let c₃ be Element of (product c₂);
let c₄ be Element of c₁;
redefine func . as c₃ . c₄ -> Element of (a₂ . a₄);
coherence

proof end;

end;

theorem Th29: :: WAYBEL_3:29

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is transitive ) holds
product b₂ is transitive

proof end;

theorem Th30: :: WAYBEL_3:30

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is antisymmetric ) holds
product b₂ is antisymmetric

proof end;

theorem Th31: :: WAYBEL_3:31

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is complete LATTICE ) holds
product b₂ is complete LATTICE

proof end;

theorem Th32: :: WAYBEL_3:32

proof end;

theorem Th33: :: WAYBEL_3:33

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is complete LATTICE ) holds
for b₃, b₄ being Element of (product b₂) holds
( b₃ << b₄ iff ( ( for b₅ being Element of b₁ holds b₃ . b₅ << b₄ . b₅ ) & ex b₅ being finite Subset of b₁ st
for b₆ being Element of b₁ st not b₆ in b₅ holds
b₃ . b₆ = Bottom (b₂ . b₆) ) )

proof end;

theorem Th34: :: WAYBEL_3:34

for b₁ being non empty TopSpace
for b₂, b₃ being Element of (InclPoset the topology of b₁) st b₂ is_way_below b₃ holds
for b₄ being Subset-Family of b₁ st b₄ is open & b₃ c= union b₄ holds
ex b₅ being finite Subset of b₄ st b₂ c= union b₅

proof end;

theorem Th35: :: WAYBEL_3:35

for b₁ being non empty TopSpace
for b₂, b₃ being Element of (InclPoset the topology of b₁) st ( for b₄ being Subset-Family of b₁ st b₄ is open & b₃ c= union b₄ holds
ex b₅ being finite Subset of b₄ st b₂ c= union b₅ ) holds
b₂ is_way_below b₃

proof end;

theorem Th36: :: WAYBEL_3:36

for b₁ being non empty TopSpace
for b₂ being Element of (InclPoset the topology of b₁)
for b₃ being Subset of b₁ st b₂ = b₃ holds
( b₂ is compact iff b₃ is compact )

proof end;

theorem Th37: :: WAYBEL_3:37

for b₁ being non empty TopSpace
for b₂ being Element of (InclPoset the topology of b₁) st b₂ = the carrier of b₁ holds
( b₂ is compact iff b₁ is compact )

proof end;

definition

let c₁ be non empty TopSpace;
attr a₁ is locally-compact means :Def9: :: WAYBEL_3:def 9
for b₁ being Point of a₁
for b₂ being Subset of a₁ st b₁ in b₂ & b₂ is open holds
ex b₃ being Subset of a₁ st
( b₁ in Int b₃ & b₃ c= b₂ & b₃ is compact );

end;

:: deftheorem Def9 defines locally-compact WAYBEL_3:def 9 :

registration

cluster non empty compact being_T2 -> non empty being_T3 being_T4 locally-compact TopStruct ;
coherence

proof end;

end;

theorem Th38: :: WAYBEL_3:38

for b₁ being set holds 1TopSp {b₁} is being_T2

proof end;

registration

cluster non empty compact being_T2 being_T3 being_T4 locally-compact TopStruct ;
existence

proof end;

end;

theorem Th39: :: WAYBEL_3:39

for b₁ being non empty TopSpace
for b₂, b₃ being Element of (InclPoset the topology of b₁) st ex b₄ being Subset of b₁ st
( b₂ c= b₄ & b₄ c= b₃ & b₄ is compact ) holds
b₂ << b₃

proof end;

theorem Th40: :: WAYBEL_3:40

for b₁ being non empty TopSpace st b₁ is locally-compact holds
for b₂, b₃ being Element of (InclPoset the topology of b₁) st b₂ << b₃ holds
ex b₄ being Subset of b₁ st
( b₂ c= b₄ & b₄ c= b₃ & b₄ is compact )

proof end;

theorem Th41: :: WAYBEL_3:41

for b₁ being non empty TopSpace st b₁ is locally-compact & b₁ is_T2 holds
for b₂, b₃ being Element of (InclPoset the topology of b₁) st b₂ << b₃ holds
ex b₄ being Subset of b₁ st
( b₄ = b₂ & Cl b₄ c= b₃ & Cl b₄ is compact )

proof end;

theorem Th42: :: WAYBEL_3:42

for b₁ being non empty TopSpace st b₁ is_T3 & InclPoset the topology of b₁ is continuous holds
b₁ is locally-compact

proof end;

theorem Th43: :: WAYBEL_3:43

for b₁ being non empty TopSpace st b₁ is locally-compact holds
InclPoset the topology of b₁ is continuous

proof end;