:: The "Way-Below" Relation
:: by Grzegorz Bancerek
::
:: Received October 11, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

definition
let L be non empty reflexive RelStr ;
let x, y be Element of L;
predx 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 &amp; x <= d );
end;

:: deftheorem Def1 defines is_way_below WAYBEL_3:def_1_:_
 for L being non empty reflexive RelStr
for x, y being Element of L holds
( x is_way_below y iff for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D &amp; x <= d ) );

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;
attrx is compact  means :Def2: :: WAYBEL_3:def 2
x is_way_below x;
end;

:: deftheorem Def2 defines compact WAYBEL_3:def_2_:_
 for L being non empty reflexive RelStr
for x being Element of L holds
( x is compact iff x is_way_below x );

notation
let L be non empty reflexive RelStr ;
let x be Element of L;
synonym  isolated_from_below x for  compact ;
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
proofend;

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 &amp; x << y &amp; y <= z holds
u << z
proofend;

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 &amp; y << z holds
( ex_sup_of {x,y},L &amp; x "\/" y << z )
proofend;

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
proofend;

theorem :: WAYBEL_3:5
for L being non empty Poset
for x, y, z being Element of L st x << y &amp; y << z holds
x << z
proofend;

theorem :: WAYBEL_3:6
for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st x << y &amp; x >> y holds
x = y
proofend;

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
proofend;
func waybelow x ->  Subset of L equals :: WAYBEL_3:def 3
 {  y where y is Element of L : y << x  }  ;
correctness
coherence
{  y where y is Element of L : y << x  }  is Subset of L;
by A1;
A2:  {  y where y is Element of L : y >> x  }  c= the carrier of L
proofend;
func wayabove x ->  Subset of L equals :: WAYBEL_3:def 4
 {  y where y is Element of L : y >> x  }  ;
correctness
coherence
{  y where y is Element of L : y >> x  }  is Subset of L;
by A2;
end;

:: deftheorem  defines waybelow WAYBEL_3:def_3_:_
 for L being non empty reflexive RelStr
for x being Element of L holds waybelow x =  {  y where y is Element of L : y << x  }  ;

:: deftheorem  defines wayabove WAYBEL_3:def_4_:_
 for L being non empty reflexive RelStr
for x being Element of L holds wayabove x =  {  y where y is Element of L : y >> x  }  ;

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 )
proofend;

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 )
proofend;

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
proofend;

theorem :: WAYBEL_3:10
for L being non empty reflexive antisymmetric RelStr
for x being Element of L holds x is_<=_than wayabove x
proofend;

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 &amp; wayabove x c= uparrow x )
proofend;

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 &amp; wayabove y c= wayabove x )
proofend;

registration
let L be non empty reflexive antisymmetric lower-bounded RelStr ;
let x be Element of L;
cluster waybelow x ->  non empty ;
coherence
 not waybelow x is empty
proofend;
end;

registration
let L be non empty reflexive transitive RelStr ;
let x be Element of L;
cluster waybelow x ->  lower ;
coherence
 waybelow x is lower
proofend;
cluster wayabove x ->  upper ;
coherence
 wayabove x is upper
proofend;
end;

registration
let L be sup-Semilattice;
let x be Element of L;
cluster waybelow x ->  directed ;
coherence
 waybelow x is directed
proofend;
end;

registration
let L be non empty /\-complete Poset;
let x be Element of L;
cluster waybelow x ->  directed ;
coherence
 waybelow x is directed
proofend;
end;

:: EXAMPLES, 1.3, p. 39
registration
let L be non empty connected RelStr ;
cluster  ->  directed filtered for Element of K10( the carrier of L);
coherence
 for b1 being Subset of L holds
( b1 is directed &amp; b1 is filtered )
proofend;
end;

registration
cluster non empty reflexive transitive antisymmetric lower-bounded connected up-complete  ->  complete for RelStr ;
coherence
 for b1 being Chain st b1 is up-complete &amp; b1 is lower-bounded holds
b1 is complete
proofend;
end;

registration
cluster non empty V233() reflexive transitive antisymmetric complete connected for RelStr ;
existence
 ex b1 being Chain st b1 is complete
proofend;
end;

theorem Th13: :: WAYBEL_3:13
for L being up-complete Chain
for x, y being Element of L st x < y holds
x << y
proofend;

theorem :: WAYBEL_3:14
for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st not x is compact &amp; x << y holds
x < y
proofend;

theorem :: WAYBEL_3:15
for L being non empty reflexive antisymmetric lower-bounded RelStr holds Bottom L is compact
proofend;

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
proofend;

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 isolated_from_below
proofend;

begin

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 &amp; x <= sup A )
proofend;

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 &amp; x <= sup A ) ) holds
x << y
proofend;

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
proofend;

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
proofend;

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 )
proofend;

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 &amp; ( for y being Element of L st y in X holds
not x < y ) ) )
proofend;

begin

definition
let L be non empty reflexive RelStr ;
attrL 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_:_
 for L being non empty reflexive RelStr holds
( L is satisfying_axiom_of_approximation iff for x being Element of L holds x = sup (waybelow x) );

registration
cluster1 -element reflexive  -> 1 -element reflexive satisfying_axiom_of_approximation for RelStr ;
coherence
 for b1 being 1 -element reflexive RelStr holds b1 is satisfying_axiom_of_approximation
proofend;
end;

definition
let L be non empty reflexive RelStr ;
attrL is continuous  means :Def6: :: WAYBEL_3:def 6
( ( for x being Element of L holds
( not waybelow x is empty &amp; waybelow x is directed ) ) &amp; L is up-complete &amp; L is satisfying_axiom_of_approximation );
end;

:: deftheorem Def6 defines continuous WAYBEL_3:def_6_:_
 for L being non empty reflexive RelStr holds
( L is continuous iff ( ( for x being Element of L holds
( not waybelow x is empty &amp; waybelow x is directed ) ) &amp; L is up-complete &amp; L is satisfying_axiom_of_approximation ) );

registration
cluster non empty reflexive continuous  ->  non empty reflexive up-complete satisfying_axiom_of_approximation for RelStr ;
coherence
 for b1 being non empty reflexive RelStr st b1 is continuous holds
( b1 is up-complete &amp; b1 is satisfying_axiom_of_approximation ) by Def6;
cluster reflexive transitive antisymmetric lower-bounded with_suprema up-complete satisfying_axiom_of_approximation  ->  lower-bounded continuous for RelStr ;
coherence
 for b1 being lower-bounded sup-Semilattice st b1 is up-complete &amp; b1 is satisfying_axiom_of_approximation holds
b1 is continuous
proofend;
end;

registration
cluster non empty strict V233() reflexive transitive antisymmetric with_suprema with_infima complete continuous for RelStr ;
existence
 ex b1 being LATTICE st
( b1 is continuous &amp; b1 is complete &amp; b1 is strict )
proofend;
end;

registration
let L be non empty reflexive continuous RelStr ;
let x be Element of L;
cluster waybelow x ->  non empty directed ;
coherence
 ( not waybelow x is empty &amp; waybelow x is directed ) 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 &amp; 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 &amp; not u <= y ) )
proofend;

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 )
proofend;

registration
cluster non empty reflexive transitive antisymmetric complete connected  ->  satisfying_axiom_of_approximation for RelStr ;
coherence
 for b1 being Chain st b1 is complete holds
b1 is satisfying_axiom_of_approximation
proofend;
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
proofend;

begin

definition
let f be Relation;
attrf is non-Empty  means :Def7: :: WAYBEL_3:def 7
 for S being 1-sorted st S in rng f holds
not S is empty ;
attrf 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_:_
 for f being Relation holds
( f is non-Empty iff for S being 1-sorted st S in rng f holds
not S is empty );

:: deftheorem Def8 defines reflexive-yielding WAYBEL_3:def_8_:_
 for f being Relation holds
( f is reflexive-yielding iff for S being RelStr st S in rng f holds
S is reflexive );

registration
let I be set ;
cluster Relation-like I -defined Function-like V31(I) RelStr-yielding non-Empty reflexive-yielding for set ;
existence
 ex b1 being ManySortedSet of I st
( b1 is RelStr-yielding &amp; b1 is non-Empty &amp; b1 is reflexive-yielding )
proofend;
end;

registration
let I be set ;
let J be RelStr-yielding non-Empty ManySortedSet of I;
cluster product J ->  non empty ;
coherence
 not product J is empty
proofend;
end;

definition
let I be non empty set ;
let J be RelStr-yielding ManySortedSet of I;
let i be Element of I;
:: original:.
redefine funcJ . i ->  RelStr ;
coherence
 J . i is RelStr
proofend;
end;

registration
let I be non empty set ;
let J be RelStr-yielding non-Empty ManySortedSet of I;
let i be Element of I;
clusterJ . i ->  non empty for RelStr ;
coherence
 for b1 being RelStr st b1 = J . i holds
not b1 is empty
proofend;
end;

registration
let I be set ;
let J be RelStr-yielding non-Empty ManySortedSet of I;
cluster product J ->  constituted-Functions ;
coherence
 product J is constituted-Functions
proofend;
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 funcx . i ->  Element of (J . i);
coherence
 x . i is Element of (J . i)
proofend;
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
 pi (X,i) is Subset of (J . i)
proofend;
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 &amp; ( for i being Element of I holds x . i is Element of (J . i) ) ) )
proofend;

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 )
proofend;

registration
let I be non empty set ;
let J be RelStr-yielding reflexive-yielding ManySortedSet of I;
let i be Element of I;
clusterJ . i ->  reflexive for RelStr ;
coherence
 for b1 being RelStr st b1 = J . i holds
b1 is reflexive
proofend;
end;

registration
let I be non empty set ;
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
cluster product J ->  reflexive ;
coherence
 product J is reflexive
proofend;
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
proofend;

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
proofend;

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
proofend;

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))
proofend;

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 ) &amp; 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) ) )
proofend;

begin

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 &amp; y c= union F holds
ex G being finite Subset of F st x c= union G
proofend;

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 &amp; y c= union F holds
ex G being finite Subset of F st x c= union G ) holds
x is_way_below y
proofend;

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 )
proofend;

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 )
proofend;

definition
let T be non empty TopSpace;
attrT 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 &amp; X is open holds
ex Y being Subset of T st
( x in Int Y &amp; Y c= X &amp; Y is compact );
end;

:: deftheorem Def9 defines locally-compact WAYBEL_3:def_9_:_
 for T being non empty TopSpace holds
( T is locally-compact iff for x being Point of T
for X being Subset of T st x in X &amp; X is open holds
ex Y being Subset of T st
( x in Int Y &amp; Y c= X &amp; Y is compact ) );

registration
cluster non empty TopSpace-like T_2 compact  ->  non empty regular normal locally-compact for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is compact &amp; b1 is T_2 holds
( b1 is regular &amp; b1 is normal &amp; b1 is locally-compact )
proofend;
end;

registration
cluster non empty TopSpace-like T_2 compact for TopStruct ;
existence
 ex b1 being non empty TopSpace st
( b1 is compact &amp; b1 is T_2 )
proofend;
end;

theorem Th38: :: WAYBEL_3:38
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 &amp; Z c= y &amp; Z is compact ) holds
x << y
proofend;

theorem Th39: :: WAYBEL_3:39
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 &amp; Z c= y &amp; Z is compact )
proofend;

theorem :: WAYBEL_3:40
for T being non empty TopSpace st T is locally-compact &amp; T is T_2 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 &amp; Cl Z c= y &amp; Cl Z is compact )
proofend;

theorem :: WAYBEL_3:41
for X being non empty TopSpace st X is regular &amp; InclPoset the topology of X is continuous holds
X is locally-compact
proofend;

theorem :: WAYBEL_3:42
for T being non empty TopSpace st T is locally-compact holds
InclPoset the topology of T is continuous
proofend;