:: WAYBEL_3 semantic presentation

definition

let L be non empty reflexive RelStr ;
let x, y be Element of L;
pred x is_way_below y means :Def1: :: WAYBEL_3:def 1
for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x <= d );

end;

:: deftheorem Def1 defines is_way_below WAYBEL_3:def 1 :

notation

let L be non empty reflexive RelStr ;
let x, y be Element of L;
synonym x << y for x is_way_below y;
synonym y >> x for x is_way_below y;

end;

definition

let L be non empty reflexive RelStr ;
let x be Element of L;
attr x is compact means :Def2: :: WAYBEL_3:def 2
x is_way_below x;

end;

:: deftheorem Def2 defines compact WAYBEL_3:def 2 :

notation

let L be non empty reflexive RelStr ;
let x be Element of L;
synonym isolated_from_below x for compact x;

end;

theorem Th1: :: WAYBEL_3:1

for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st x << y holds
x <= y

proof end;

theorem Th2: :: WAYBEL_3:2

for L being non empty reflexive transitive RelStr
for u, x, y, z being Element of L st u <= x & x << y & y <= z holds
u << z

proof end;

theorem Th3: :: WAYBEL_3:3

for L being non empty Poset st ( L is with_suprema or L is /\-complete ) holds
for x, y, z being Element of L st x << z & y << z holds
( ex_sup_of {x,y},L & x "\/" y << z )

proof end;

theorem Th4: :: WAYBEL_3:4

for L being non empty reflexive antisymmetric lower-bounded RelStr
for x being Element of L holds Bottom L << x

proof end;

theorem :: WAYBEL_3:5

for L being non empty Poset
for x, y, z being Element of L st x << y & y << z holds
x << z

proof end;

theorem :: WAYBEL_3:6

for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st x << y & x >> y holds
x = y

proof end;

definition

let L be non empty reflexive RelStr ;
let x be Element of L;
A1: { y where y is Element of L : y << x } c= the carrier of L

proof end;

func waybelow x -> Subset of L equals :: WAYBEL_3:def 3
{ y where y is Element of L : y << x } ;
correctness by A1;
A2: { y where y is Element of L : y >> x } c= the carrier of L

proof end;

func wayabove x -> Subset of L equals :: WAYBEL_3:def 4
{ y where y is Element of L : y >> x } ;
correctness by A2;

end;

:: deftheorem defines waybelow WAYBEL_3:def 3 :

:: deftheorem defines wayabove WAYBEL_3:def 4 :

theorem Th7: :: WAYBEL_3:7

for L being non empty reflexive RelStr
for x, y being Element of L holds
( x in waybelow y iff x << y )

proof end;

theorem Th8: :: WAYBEL_3:8

for L being non empty reflexive RelStr
for x, y being Element of L holds
( x in wayabove y iff x >> y )

proof end;

theorem Th9: :: WAYBEL_3:9

for L being non empty reflexive antisymmetric RelStr
for x being Element of L holds x is_>=_than waybelow x

proof end;

theorem :: WAYBEL_3:10

for L being non empty reflexive antisymmetric RelStr
for x being Element of L holds x is_<=_than wayabove x

proof end;

theorem Th11: :: WAYBEL_3:11

for L being non empty reflexive antisymmetric RelStr
for x being Element of L holds
( waybelow x c= downarrow x & wayabove x c= uparrow x )

proof end;

theorem Th12: :: WAYBEL_3:12

for L being non empty reflexive transitive RelStr
for x, y being Element of L st x <= y holds
( waybelow x c= waybelow y & wayabove y c= wayabove x )

proof end;

registration

let L be non empty reflexive antisymmetric lower-bounded RelStr ;
let x be Element of L;
cluster waybelow x -> non empty ;
coherence

proof end;

end;

registration

let L be non empty reflexive transitive RelStr ;
let x be Element of L;
cluster waybelow x -> lower ;
coherence

proof end;

cluster wayabove x -> upper ;
coherence

proof end;

end;

registration

let L be sup-Semilattice;
let x be Element of L;
cluster waybelow x -> directed lower ;
coherence

proof end;

end;

registration

let L be non empty /\-complete Poset;
let x be Element of L;
cluster waybelow x -> non empty directed lower ;
coherence

proof end;

end;

registration

let L be non empty connected RelStr ;
cluster -> directed filtered Element of K40(the carrier of L);
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 L being non empty up-complete Chain
for x, y being Element of L st x < y holds
x << y

proof end;

theorem :: WAYBEL_3:14

for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st not x is compact & x << y holds
x < y

proof end;

theorem :: WAYBEL_3:15

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

proof end;

theorem Th16: :: WAYBEL_3:16

for L being non empty up-complete Poset
for D being non empty finite directed Subset of L holds sup D in D

proof end;

theorem :: WAYBEL_3:17

for L being non empty up-complete Poset st L is finite holds
for x being Element of L holds x is compact

proof end;

theorem Th18: :: WAYBEL_3:18

for L being complete LATTICE
for x, y being Element of L st x << y holds
for X being Subset of L st y <= sup X holds
ex A being finite Subset of L st
( A c= X & x <= sup A )

proof end;

theorem :: WAYBEL_3:19

for L being complete LATTICE
for x, y being Element of L st ( for X being Subset of L st y <= sup X holds
ex A being finite Subset of L st
( A c= X & x <= sup A ) ) holds
x << y

proof end;

theorem :: WAYBEL_3:20

for L being non empty reflexive transitive RelStr
for x, y being Element of L st x << y holds
for I being Ideal of L st y <= sup I holds
x in I

proof end;

theorem Th21: :: WAYBEL_3:21

for L being non empty up-complete Poset
for x, y being Element of L st ( for I being Ideal of L st y <= sup I holds
x in I ) holds
x << y

proof end;

theorem :: WAYBEL_3:22

for L being lower-bounded LATTICE st L is meet-continuous holds
for x, y being Element of L holds
( x << y iff for I being Ideal of L st y = sup I holds
x in I )

proof end;

theorem :: WAYBEL_3:23

for L being complete LATTICE holds
( ( for x being Element of L holds x is compact ) iff for X being non empty Subset of L ex x being Element of L st
( x in X & ( for y being Element of L st y in X holds
not x < y ) ) )

proof end;

definition

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

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 L be non empty reflexive RelStr ;
attr L is continuous means :Def6: :: WAYBEL_3:def 6
( ( for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ) & L is up-complete & L 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 L be non empty reflexive continuous RelStr ;
let x be Element of L;
cluster waybelow x -> non empty directed ;
coherence by Def6;

end;

theorem :: WAYBEL_3:24

for L being up-complete Semilattice st ( for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ) holds
( L is satisfying_axiom_of_approximation iff for x, y being Element of L st not x <= y holds
ex u being Element of L st
( u << x & not u <= y ) )

proof end;

theorem :: WAYBEL_3:25

for L being continuous LATTICE
for x, y being Element of L holds
( x <= y iff waybelow x c= waybelow y )

proof end;

registration

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

proof end;

end;

theorem :: WAYBEL_3:26

for L being complete LATTICE st ( for x being Element of L holds x is compact ) holds
L is satisfying_axiom_of_approximation

proof end;

definition

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

end;

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

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

registration

let I be set ;
cluster RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
existence

proof end;

end;

registration

let I be set ;
let J be RelStr-yielding non-Empty ManySortedSet of I;
cluster product J -> non empty ;
coherence

proof end;

end;

definition

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

proof end;

end;

registration

let I be set ;
let J be RelStr-yielding non-Empty ManySortedSet of I;
cluster product J -> non empty constituted-Functions ;
coherence

proof end;

end;

definition

let I be non empty set ;
let J be RelStr-yielding non-Empty ManySortedSet of I;
let x be Element of (product J);
let i be Element of I;
:: original: .
redefine func x . i -> Element of (J . i);
coherence

proof end;

end;

definition

let I be non empty set ;
let J be RelStr-yielding non-Empty ManySortedSet of I;
let i be Element of I;
let X be Subset of (product J);
:: original: pi
redefine func pi X,i -> Subset of (J . i);
coherence

proof end;

end;

theorem Th27: :: WAYBEL_3:27

for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I
for x being Function holds
( x is Element of (product J) iff ( dom x = I & ( for i being Element of I holds x . i is Element of (J . i) ) ) )

proof end;

theorem Th28: :: WAYBEL_3:28

for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I
for x, y being Element of (product J) holds
( x <= y iff for i being Element of I holds x . i <= y . i )

proof end;

definition

let I be non empty set ;
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
let i be Element of I;
:: original: .
redefine func J . i -> non empty reflexive RelStr ;
coherence

proof end;

end;

registration

let I be non empty set ;
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
cluster product J -> non empty reflexive constituted-Functions ;
coherence

proof end;

end;

definition

let I be non empty set ;
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
let x be Element of (product J);
let i be Element of I;
:: original: .
redefine func x . i -> Element of (J . i);
coherence

proof end;

end;

theorem Th29: :: WAYBEL_3:29

for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is transitive ) holds
product J is transitive

proof end;

theorem Th30: :: WAYBEL_3:30

for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric ) holds
product J is antisymmetric

proof end;

theorem Th31: :: WAYBEL_3:31

for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds
product J is complete LATTICE

proof end;

theorem Th32: :: WAYBEL_3:32

for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds
for X being Subset of (product J)
for i being Element of I holds (sup X) . i = sup (pi X,i)

proof end;

theorem :: WAYBEL_3:33

for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds
for x, y being Element of (product J) holds
( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) ) )

proof end;

theorem Th34: :: WAYBEL_3:34

for T being non empty TopSpace
for x, y being Element of (InclPoset the topology of T) st x is_way_below y holds
for F being Subset-Family of T st F is open & y c= union F holds
ex G being finite Subset of F st x c= union G

proof end;

theorem Th35: :: WAYBEL_3:35

for T being non empty TopSpace
for x, y being Element of (InclPoset the topology of T) st ( for F being Subset-Family of T st F is open & y c= union F holds
ex G being finite Subset of F st x c= union G ) holds
x is_way_below y

proof end;

theorem Th36: :: WAYBEL_3:36

for T being non empty TopSpace
for x being Element of (InclPoset the topology of T)
for X being Subset of T st x = X holds
( x is compact iff X is compact )

proof end;

theorem :: WAYBEL_3:37

for T being non empty TopSpace
for x being Element of (InclPoset the topology of T) st x = the carrier of T holds
( x is compact iff T is compact )

proof end;

definition

let T be non empty TopSpace;
attr T is locally-compact means :Def9: :: WAYBEL_3:def 9
for x being Point of T
for X being Subset of T st x in X & X is open holds
ex Y being Subset of T st
( x in Int Y & Y c= X & Y 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 x being set holds 1TopSp {x} 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 T being non empty TopSpace
for x, y being Element of (InclPoset the topology of T) st ex Z being Subset of T st
( x c= Z & Z c= y & Z is compact ) holds
x << y

proof end;

theorem Th40: :: WAYBEL_3:40

for T being non empty TopSpace st T is locally-compact holds
for x, y being Element of (InclPoset the topology of T) st x << y holds
ex Z being Subset of T st
( x c= Z & Z c= y & Z is compact )

proof end;

theorem :: WAYBEL_3:41

for T being non empty TopSpace st T is locally-compact & T is_T2 holds
for x, y being Element of (InclPoset the topology of T) st x << y holds
ex Z being Subset of T st
( Z = x & Cl Z c= y & Cl Z is compact )

proof end;

theorem :: WAYBEL_3:42

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

proof end;

theorem :: WAYBEL_3:43

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

proof end;