:: ISOMICHI semantic presentation
begin
registration
let D be non trivial set ;
cluster ADTS D -> non trivial ;
coherence
not ADTS D is trivial
proof
ADTS D = TopStruct(# D,(cobool D) #) by TEX_1:def_3;
hence not ADTS D is trivial ; ::_thesis: verum
end;
end;
registration
cluster non trivial strict TopSpace-like anti-discrete for TopStruct ;
existence
ex b1 being TopSpace st
( b1 is anti-discrete & not b1 is trivial & b1 is strict )
proof
set D = the non trivial set ;
take ADTS the non trivial set ; ::_thesis: ( ADTS the non trivial set is anti-discrete & not ADTS the non trivial set is trivial & ADTS the non trivial set is strict )
thus ( ADTS the non trivial set is anti-discrete & not ADTS the non trivial set is trivial & ADTS the non trivial set is strict ) ; ::_thesis: verum
end;
end;
theorem Th1: :: ISOMICHI:1
for T being TopSpace
for A, B being Subset of T holds (Int (Cl (Int A))) /\ (Int (Cl (Int B))) = Int (Cl (Int (A /\ B)))
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T holds (Int (Cl (Int A))) /\ (Int (Cl (Int B))) = Int (Cl (Int (A /\ B)))
let A, B be Subset of T; ::_thesis: (Int (Cl (Int A))) /\ (Int (Cl (Int B))) = Int (Cl (Int (A /\ B)))
set C = Int A;
set D = Int B;
(Int (Cl (Int A))) /\ (Int (Cl (Int B))) = Int (Cl ((Int A) /\ (Int B))) by TDLAT_1:7;
hence (Int (Cl (Int A))) /\ (Int (Cl (Int B))) = Int (Cl (Int (A /\ B))) by TOPS_1:17; ::_thesis: verum
end;
theorem Th2: :: ISOMICHI:2
for T being TopSpace
for A, B being Subset of T holds Cl (Int (Cl (A \/ B))) = (Cl (Int (Cl A))) \/ (Cl (Int (Cl B)))
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T holds Cl (Int (Cl (A \/ B))) = (Cl (Int (Cl A))) \/ (Cl (Int (Cl B)))
let A, B be Subset of T; ::_thesis: Cl (Int (Cl (A \/ B))) = (Cl (Int (Cl A))) \/ (Cl (Int (Cl B)))
set C = Cl A;
set D = Cl B;
(Cl (Int (Cl A))) \/ (Cl (Int (Cl B))) = Cl (Int ((Cl A) \/ (Cl B))) by TDLAT_1:6;
hence Cl (Int (Cl (A \/ B))) = (Cl (Int (Cl A))) \/ (Cl (Int (Cl B))) by PRE_TOPC:20; ::_thesis: verum
end;
begin
definition
let T be TopStruct ;
let A be Subset of T;
attrA is supercondensed means :Def1: :: ISOMICHI:def 1
Int (Cl A) = Int A;
attrA is subcondensed means :Def2: :: ISOMICHI:def 2
Cl (Int A) = Cl A;
end;
:: deftheorem Def1 defines supercondensed ISOMICHI:def_1_:_
for T being TopStruct
for A being Subset of T holds
( A is supercondensed iff Int (Cl A) = Int A );
:: deftheorem Def2 defines subcondensed ISOMICHI:def_2_:_
for T being TopStruct
for A being Subset of T holds
( A is subcondensed iff Cl (Int A) = Cl A );
registration
let T be TopSpace;
cluster closed -> supercondensed for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is closed holds
b1 is supercondensed
proof
let A be Subset of T; ::_thesis: ( A is closed implies A is supercondensed )
assume A is closed ; ::_thesis: A is supercondensed
then Int (Cl A) = Int A by PRE_TOPC:22;
hence A is supercondensed by Def1; ::_thesis: verum
end;
end;
theorem :: ISOMICHI:3
for T being TopSpace
for A being Subset of T st A is closed holds
A is supercondensed ;
theorem Th4: :: ISOMICHI:4
for T being TopSpace
for A being Subset of T st A is open holds
A is subcondensed
proof
let T be TopSpace; ::_thesis: for A being Subset of T st A is open holds
A is subcondensed
let A be Subset of T; ::_thesis: ( A is open implies A is subcondensed )
assume A is open ; ::_thesis: A is subcondensed
then Cl (Int A) = Cl A by TOPS_1:23;
hence A is subcondensed by Def2; ::_thesis: verum
end;
definition
let T be TopSpace;
let A be Subset of T;
redefine attr A is condensed means :Def3: :: ISOMICHI:def 3
( Cl (Int A) = Cl A & Int (Cl A) = Int A );
compatibility
( A is condensed iff ( Cl (Int A) = Cl A & Int (Cl A) = Int A ) )
proof
thus ( A is condensed implies ( Cl (Int A) = Cl A & Int (Cl A) = Int A ) ) by TDLAT_3:9; ::_thesis: ( Cl (Int A) = Cl A & Int (Cl A) = Int A implies A is condensed )
assume that
A1: Cl (Int A) = Cl A and
A2: Int (Cl A) = Int A ; ::_thesis: A is condensed
A3: Int A c= A by TOPS_1:16;
A c= Cl (Int A) by A1, PRE_TOPC:18;
hence A is condensed by A2, A3, TOPS_1:def_6; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines condensed ISOMICHI:def_3_:_
for T being TopSpace
for A being Subset of T holds
( A is condensed iff ( Cl (Int A) = Cl A & Int (Cl A) = Int A ) );
theorem Th5: :: ISOMICHI:5
for T being TopSpace
for A being Subset of T holds
( A is condensed iff ( A is subcondensed & A is supercondensed ) )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is condensed iff ( A is subcondensed & A is supercondensed ) )
let A be Subset of T; ::_thesis: ( A is condensed iff ( A is subcondensed & A is supercondensed ) )
thus ( A is condensed implies ( A is subcondensed & A is supercondensed ) ) ::_thesis: ( A is subcondensed & A is supercondensed implies A is condensed )
proof
assume A1: A is condensed ; ::_thesis: ( A is subcondensed & A is supercondensed )
then A2: Int (Cl A) = Int A by Def3;
Cl (Int A) = Cl A by A1, Def3;
hence ( A is subcondensed & A is supercondensed ) by A2, Def1, Def2; ::_thesis: verum
end;
assume that
A3: A is subcondensed and
A4: A is supercondensed ; ::_thesis: A is condensed
A5: Cl (Int A) = Cl A by A3, Def2;
Int (Cl A) = Int A by A4, Def1;
hence A is condensed by A5, Def3; ::_thesis: verum
end;
registration
let T be TopSpace;
cluster condensed -> supercondensed subcondensed for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is condensed holds
( b1 is subcondensed & b1 is supercondensed ) by Th5;
cluster supercondensed subcondensed -> condensed for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is subcondensed & b1 is supercondensed holds
b1 is condensed by Th5;
end;
registration
let T be TopSpace;
cluster condensed supercondensed subcondensed for Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( b1 is condensed & b1 is subcondensed & b1 is supercondensed )
proof
set A = {} T;
take {} T ; ::_thesis: ( {} T is condensed & {} T is subcondensed & {} T is supercondensed )
( {} T is supercondensed & {} T is subcondensed ) by Th4;
hence ( {} T is condensed & {} T is subcondensed & {} T is supercondensed ) ; ::_thesis: verum
end;
end;
theorem :: ISOMICHI:6
for T being TopSpace
for A being Subset of T st A is supercondensed holds
A ` is subcondensed
proof
let T be TopSpace; ::_thesis: for A being Subset of T st A is supercondensed holds
A ` is subcondensed
let A be Subset of T; ::_thesis: ( A is supercondensed implies A ` is subcondensed )
A1: (Int A) ` = Cl (A `) by TDLAT_3:2;
assume A is supercondensed ; ::_thesis: A ` is subcondensed
then A2: (Int (Cl A)) ` = (Int A) ` by Def1;
(Int (Cl A)) ` = Cl ((Cl A) `) by TDLAT_3:2
.= Cl (Int (A `)) by TDLAT_3:3 ;
hence A ` is subcondensed by A2, A1, Def2; ::_thesis: verum
end;
theorem :: ISOMICHI:7
for T being TopSpace
for A being Subset of T st A is subcondensed holds
A ` is supercondensed
proof
let T be TopSpace; ::_thesis: for A being Subset of T st A is subcondensed holds
A ` is supercondensed
let A be Subset of T; ::_thesis: ( A is subcondensed implies A ` is supercondensed )
A1: (Cl A) ` = Int (A `) by TDLAT_3:3;
assume A is subcondensed ; ::_thesis: A ` is supercondensed
then A2: (Cl (Int A)) ` = (Cl A) ` by Def2;
(Cl (Int A)) ` = Int ((Int A) `) by TDLAT_3:3
.= Int (Cl (A `)) by TDLAT_3:2 ;
hence A ` is supercondensed by A2, A1, Def1; ::_thesis: verum
end;
theorem Th8: :: ISOMICHI:8
for T being TopSpace
for A being Subset of T holds
( A is supercondensed iff Int (Cl A) c= A )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is supercondensed iff Int (Cl A) c= A )
let A be Subset of T; ::_thesis: ( A is supercondensed iff Int (Cl A) c= A )
thus ( A is supercondensed implies Int (Cl A) c= A ) ::_thesis: ( Int (Cl A) c= A implies A is supercondensed )
proof
assume A is supercondensed ; ::_thesis: Int (Cl A) c= A
then Int (Cl A) = Int A by Def1;
hence Int (Cl A) c= A by TOPS_1:16; ::_thesis: verum
end;
assume Int (Cl A) c= A ; ::_thesis: A is supercondensed
then A1: Int (Int (Cl A)) c= Int A by TOPS_1:19;
Int A c= Int (Cl A) by PRE_TOPC:18, TOPS_1:19;
then Int A = Int (Cl A) by A1, XBOOLE_0:def_10;
hence A is supercondensed by Def1; ::_thesis: verum
end;
theorem Th9: :: ISOMICHI:9
for T being TopSpace
for A being Subset of T holds
( A is subcondensed iff A c= Cl (Int A) )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is subcondensed iff A c= Cl (Int A) )
let A be Subset of T; ::_thesis: ( A is subcondensed iff A c= Cl (Int A) )
thus ( A is subcondensed implies A c= Cl (Int A) ) ::_thesis: ( A c= Cl (Int A) implies A is subcondensed )
proof
assume A is subcondensed ; ::_thesis: A c= Cl (Int A)
then Cl (Int A) = Cl A by Def2;
hence A c= Cl (Int A) by PRE_TOPC:18; ::_thesis: verum
end;
assume A c= Cl (Int A) ; ::_thesis: A is subcondensed
then A1: Cl A c= Cl (Cl (Int A)) by PRE_TOPC:19;
Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16;
then Cl (Int A) = Cl A by A1, XBOOLE_0:def_10;
hence A is subcondensed by Def2; ::_thesis: verum
end;
registration
let T be TopSpace;
cluster subcondensed -> semi-open for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is subcondensed holds
b1 is semi-open
proof
let A be Subset of T; ::_thesis: ( A is subcondensed implies A is semi-open )
assume A is subcondensed ; ::_thesis: A is semi-open
then A c= Cl (Int A) by Th9;
hence A is semi-open by DECOMP_1:def_2; ::_thesis: verum
end;
cluster semi-open -> subcondensed for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is semi-open holds
b1 is subcondensed
proof
let A be Subset of T; ::_thesis: ( A is semi-open implies A is subcondensed )
assume A is semi-open ; ::_thesis: A is subcondensed
then A c= Cl (Int A) by DECOMP_1:def_2;
hence A is subcondensed by Th9; ::_thesis: verum
end;
end;
theorem Th10: :: ISOMICHI:10
for T being TopSpace
for A being Subset of T holds
( A is condensed iff ( Int (Cl A) c= A & A c= Cl (Int A) ) )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is condensed iff ( Int (Cl A) c= A & A c= Cl (Int A) ) )
let A be Subset of T; ::_thesis: ( A is condensed iff ( Int (Cl A) c= A & A c= Cl (Int A) ) )
thus ( A is condensed implies ( Int (Cl A) c= A & A c= Cl (Int A) ) ) by Th8, Th9; ::_thesis: ( Int (Cl A) c= A & A c= Cl (Int A) implies A is condensed )
assume that
A1: Int (Cl A) c= A and
A2: A c= Cl (Int A) ; ::_thesis: A is condensed
A3: A is subcondensed by A2, Th9;
A is supercondensed by A1, Th8;
hence A is condensed by A3; ::_thesis: verum
end;
begin
notation
let T be TopStruct ;
let A be Subset of T;
synonym regular_open A for open_condensed ;
end;
notation
let T be TopStruct ;
let A be Subset of T;
synonym regular_closed A for closed_condensed ;
end;
theorem :: ISOMICHI:11
for T being TopSpace holds
( [#] T is regular_open & [#] T is regular_closed )
proof
let T be TopSpace; ::_thesis: ( [#] T is regular_open & [#] T is regular_closed )
A1: Int ([#] T) = [#] T by TOPS_1:15;
Cl ([#] T) = [#] T by TOPS_1:2;
hence ( [#] T is regular_open & [#] T is regular_closed ) by A1, TOPS_1:def_7, TOPS_1:def_8; ::_thesis: verum
end;
registration
let T be TopSpace;
cluster [#] T -> regular_closed regular_open ;
coherence
( [#] T is regular_open & [#] T is regular_closed )
proof
A1: Int ([#] T) = [#] T by TOPS_1:15;
Cl ([#] T) = [#] T by TOPS_1:2;
hence ( [#] T is regular_open & [#] T is regular_closed ) by A1, TOPS_1:def_7, TOPS_1:def_8; ::_thesis: verum
end;
end;
registration
let T be TopSpace;
cluster empty -> regular_closed regular_open for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is empty holds
( b1 is regular_open & b1 is regular_closed )
proof
let S be Subset of T; ::_thesis: ( S is empty implies ( S is regular_open & S is regular_closed ) )
assume A1: S is empty ; ::_thesis: ( S is regular_open & S is regular_closed )
then A2: S = Int S ;
S = Cl S by A1, PCOMPS_1:2;
hence ( S is regular_open & S is regular_closed ) by A2, TOPS_1:def_7, TOPS_1:def_8; ::_thesis: verum
end;
end;
theorem :: ISOMICHI:12
for T being TopSpace holds Int (Cl ({} T)) = {} T
proof
let T be TopSpace; ::_thesis: Int (Cl ({} T)) = {} T
Int (Cl ({} T)) = Int ({} T) by PCOMPS_1:2
.= {} T ;
hence Int (Cl ({} T)) = {} T ; ::_thesis: verum
end;
theorem Th13: :: ISOMICHI:13
for T being TopSpace
for A being Subset of T st A is regular_open holds
A ` is regular_closed
proof
let T be TopSpace; ::_thesis: for A being Subset of T st A is regular_open holds
A ` is regular_closed
let A be Subset of T; ::_thesis: ( A is regular_open implies A ` is regular_closed )
assume A is regular_open ; ::_thesis: A ` is regular_closed
then Int (Cl A) = A by TOPS_1:def_8;
then Cl ((Cl A) `) = A ` by TDLAT_3:2;
then Cl (Int (A `)) = A ` by TDLAT_3:3;
hence A ` is regular_closed by TOPS_1:def_7; ::_thesis: verum
end;
registration
let T be TopSpace;
cluster regular_closed regular_open for Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( b1 is regular_open & b1 is regular_closed )
proof
take {} T ; ::_thesis: ( {} T is regular_open & {} T is regular_closed )
thus ( {} T is regular_open & {} T is regular_closed ) ; ::_thesis: verum
end;
end;
registration
let T be TopSpace;
let A be regular_open Subset of T;
clusterA ` -> regular_closed ;
coherence
A ` is regular_closed by Th13;
end;
theorem Th14: :: ISOMICHI:14
for T being TopSpace
for A being Subset of T st A is regular_closed holds
A ` is regular_open
proof
let T be TopSpace; ::_thesis: for A being Subset of T st A is regular_closed holds
A ` is regular_open
let A be Subset of T; ::_thesis: ( A is regular_closed implies A ` is regular_open )
assume A is regular_closed ; ::_thesis: A ` is regular_open
then Cl (Int A) = A by TOPS_1:def_7;
then Int ((Int A) `) = A ` by TDLAT_3:3;
then Int (Cl (A `)) = A ` by TDLAT_3:2;
hence A ` is regular_open by TOPS_1:def_8; ::_thesis: verum
end;
registration
let T be TopSpace;
let A be regular_closed Subset of T;
clusterA ` -> regular_open ;
coherence
A ` is regular_open by Th14;
end;
registration
let T be TopSpace;
cluster regular_open -> open for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is regular_open holds
b1 is open by TOPS_1:67;
cluster regular_closed -> closed for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is regular_closed holds
b1 is closed by TOPS_1:66;
end;
theorem Th15: :: ISOMICHI:15
for T being TopSpace
for A being Subset of T holds
( Int (Cl A) is regular_open & Cl (Int A) is regular_closed )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( Int (Cl A) is regular_open & Cl (Int A) is regular_closed )
let A be Subset of T; ::_thesis: ( Int (Cl A) is regular_open & Cl (Int A) is regular_closed )
A1: Cl (Int (Cl (Int A))) = Cl (Int A) by TOPS_1:26;
Int (Cl (Int (Cl A))) = Int (Cl A) by TDLAT_1:5;
hence ( Int (Cl A) is regular_open & Cl (Int A) is regular_closed ) by A1, TOPS_1:def_7, TOPS_1:def_8; ::_thesis: verum
end;
registration
let T be TopSpace;
let A be Subset of T;
cluster Int (Cl A) -> regular_open ;
coherence
Int (Cl A) is regular_open by Th15;
cluster Cl (Int A) -> regular_closed ;
coherence
Cl (Int A) is regular_closed by Th15;
end;
theorem :: ISOMICHI:16
for T being TopSpace
for A being Subset of T holds
( A is regular_open iff ( A is supercondensed & A is open ) )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is regular_open iff ( A is supercondensed & A is open ) )
let A be Subset of T; ::_thesis: ( A is regular_open iff ( A is supercondensed & A is open ) )
thus ( A is regular_open implies ( A is supercondensed & A is open ) ) ::_thesis: ( A is supercondensed & A is open implies A is regular_open )
proof
assume A is regular_open ; ::_thesis: ( A is supercondensed & A is open )
then A1: Int (Cl A) = A by TOPS_1:def_8;
then Int A = A ;
hence ( A is supercondensed & A is open ) by A1, Def1; ::_thesis: verum
end;
assume that
A2: A is supercondensed and
A3: A is open ; ::_thesis: A is regular_open
Int (Cl A) = Int A by A2, Def1;
hence A is regular_open by A3, TOPS_1:23; ::_thesis: verum
end;
theorem :: ISOMICHI:17
for T being TopSpace
for A being Subset of T holds
( A is regular_closed iff ( A is subcondensed & A is closed ) )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is regular_closed iff ( A is subcondensed & A is closed ) )
let A be Subset of T; ::_thesis: ( A is regular_closed iff ( A is subcondensed & A is closed ) )
thus ( A is regular_closed implies ( A is subcondensed & A is closed ) ) ::_thesis: ( A is subcondensed & A is closed implies A is regular_closed )
proof
assume A is regular_closed ; ::_thesis: ( A is subcondensed & A is closed )
then A1: Cl (Int A) = A by TOPS_1:def_7;
then Cl A = A ;
hence ( A is subcondensed & A is closed ) by A1, Def2; ::_thesis: verum
end;
assume that
A2: A is subcondensed and
A3: A is closed ; ::_thesis: A is regular_closed
Cl (Int A) = Cl A by A2, Def2;
hence A is regular_closed by A3, PRE_TOPC:22; ::_thesis: verum
end;
registration
let T be TopSpace;
cluster regular_open -> open condensed for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is regular_open holds
( b1 is condensed & b1 is open ) by TOPS_1:67;
cluster open condensed -> regular_open for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is condensed & b1 is open holds
b1 is regular_open by TOPS_1:67;
cluster regular_closed -> closed condensed for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is regular_closed holds
( b1 is condensed & b1 is closed ) by TOPS_1:66;
cluster closed condensed -> regular_closed for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is condensed & b1 is closed holds
b1 is regular_closed by TOPS_1:66;
end;
theorem :: ISOMICHI:18
for T being TopSpace
for A being Subset of T holds
( A is condensed iff ex B being Subset of T st
( B is regular_open & B c= A & A c= Cl B ) )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is condensed iff ex B being Subset of T st
( B is regular_open & B c= A & A c= Cl B ) )
let A be Subset of T; ::_thesis: ( A is condensed iff ex B being Subset of T st
( B is regular_open & B c= A & A c= Cl B ) )
thus ( A is condensed implies ex B being Subset of T st
( B is regular_open & B c= A & A c= Cl B ) ) ::_thesis: ( ex B being Subset of T st
( B is regular_open & B c= A & A c= Cl B ) implies A is condensed )
proof
assume A1: A is condensed ; ::_thesis: ex B being Subset of T st
( B is regular_open & B c= A & A c= Cl B )
then A2: Cl (Int A) = Cl A by Def3;
take Int (Cl A) ; ::_thesis: ( Int (Cl A) is regular_open & Int (Cl A) c= A & A c= Cl (Int (Cl A)) )
Int (Cl A) = Int A by A1, Def3;
hence ( Int (Cl A) is regular_open & Int (Cl A) c= A & A c= Cl (Int (Cl A)) ) by A2, PRE_TOPC:18, TOPS_1:16; ::_thesis: verum
end;
given B being Subset of T such that A3: B is regular_open and
A4: B c= A and
A5: A c= Cl B ; ::_thesis: A is condensed
A6: Int (Cl B) = B by A3, TOPS_1:def_8;
Int B c= Int A by A4, TOPS_1:19;
then A7: Cl (Int B) c= Cl (Int A) by PRE_TOPC:19;
A8: Cl (Int B) = Cl B by A3, Def2;
Int A c= Int (Cl B) by A5, TOPS_1:19;
then Cl (Int A) c= Cl B by A6, PRE_TOPC:19;
then A9: Cl B = Cl (Int A) by A7, A8, XBOOLE_0:def_10;
Cl B c= Cl A by A4, PRE_TOPC:19;
then A10: Int (Cl B) c= Int (Cl A) by TOPS_1:19;
Cl A c= Cl (Cl B) by A5, PRE_TOPC:19;
then Int (Cl A) c= Int (Cl (Cl B)) by TOPS_1:19;
then B = Int (Cl A) by A6, A10, XBOOLE_0:def_10;
hence A is condensed by A4, A5, A9, Th10; ::_thesis: verum
end;
theorem :: ISOMICHI:19
for T being TopSpace
for A being Subset of T holds
( A is condensed iff ex B being Subset of T st
( B is regular_closed & Int B c= A & A c= B ) )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is condensed iff ex B being Subset of T st
( B is regular_closed & Int B c= A & A c= B ) )
let A be Subset of T; ::_thesis: ( A is condensed iff ex B being Subset of T st
( B is regular_closed & Int B c= A & A c= B ) )
thus ( A is condensed implies ex B being Subset of T st
( B is regular_closed & Int B c= A & A c= B ) ) ::_thesis: ( ex B being Subset of T st
( B is regular_closed & Int B c= A & A c= B ) implies A is condensed )
proof
assume A1: A is condensed ; ::_thesis: ex B being Subset of T st
( B is regular_closed & Int B c= A & A c= B )
then A2: Cl (Int A) = Cl A by Def3;
take Cl (Int A) ; ::_thesis: ( Cl (Int A) is regular_closed & Int (Cl (Int A)) c= A & A c= Cl (Int A) )
Int (Cl A) = Int A by A1, Def3;
hence ( Cl (Int A) is regular_closed & Int (Cl (Int A)) c= A & A c= Cl (Int A) ) by A2, PRE_TOPC:18, TOPS_1:16; ::_thesis: verum
end;
given B being Subset of T such that A3: B is regular_closed and
A4: Int B c= A and
A5: A c= B ; ::_thesis: A is condensed
A6: Cl (Int B) = B by A3, TOPS_1:def_7;
Cl A c= Cl B by A5, PRE_TOPC:19;
then Int (Cl A) c= Int (Cl B) by TOPS_1:19;
then A7: Int (Cl A) c= Int B by A3, Def1;
Cl (Int B) c= Cl A by A4, PRE_TOPC:19;
then Int B c= Int (Cl A) by A6, TOPS_1:19;
then A8: Int B = Int (Cl A) by A7, XBOOLE_0:def_10;
Int A c= Int B by A5, TOPS_1:19;
then A9: Cl (Int A) c= Cl (Int B) by PRE_TOPC:19;
Int (Int B) c= Int A by A4, TOPS_1:19;
then Cl (Int (Int B)) c= Cl (Int A) by PRE_TOPC:19;
then Cl (Int A) = B by A6, A9, XBOOLE_0:def_10;
hence A is condensed by A4, A5, A8, Th10; ::_thesis: verum
end;
begin
definition
let T be TopStruct ;
let A be Subset of T;
redefine func Fr A equals :: ISOMICHI:def 4
(Cl A) \ (Int A);
compatibility
for b1 being Element of bool the carrier of T holds
( b1 = Fr A iff b1 = (Cl A) \ (Int A) ) by TOPGEN_1:8;
end;
:: deftheorem defines Fr ISOMICHI:def_4_:_
for T being TopStruct
for A being Subset of T holds Fr A = (Cl A) \ (Int A);
theorem :: ISOMICHI:20
for T being TopSpace
for A being Subset of T holds
( A is condensed iff ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is condensed iff ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) )
let A be Subset of T; ::_thesis: ( A is condensed iff ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) )
A1: A c= Cl A by PRE_TOPC:18;
(Cl (Int A)) /\ (Cl (Int (A `))) c= Cl (Int A) by XBOOLE_1:17;
then A2: (Int A) \/ ((Cl (Int A)) /\ (Cl (Int (A `)))) c= (Int A) \/ (Cl (Int A)) by XBOOLE_1:13;
thus ( A is condensed implies ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) ) ::_thesis: ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) implies A is condensed )
proof
assume A3: A is condensed ; ::_thesis: ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) )
then A ` is condensed by TDLAT_1:16;
then A4: Cl (Int (A `)) = Cl (A `) by Def2;
Cl (Int A) = Cl A by A3, Def2;
hence ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) by A3, A4, Def1, TOPS_1:def_2; ::_thesis: verum
end;
assume that
Fr A = (Cl (Int A)) \ (Int (Cl A)) and
A5: Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ; ::_thesis: A is condensed
A6: (Cl A) \/ (Int A) = (Int A) \/ (Fr A) by XBOOLE_1:39;
Int A c= A by TOPS_1:16;
then Cl A = (Int A) \/ ((Cl (Int A)) /\ (Cl (Int (A `)))) by A5, A1, A6, XBOOLE_1:1, XBOOLE_1:12;
then A7: Cl A c= Cl (Int A) by A2, PRE_TOPC:18, XBOOLE_1:12;
Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16;
then Cl (Int A) = Cl A by A7, XBOOLE_0:def_10;
then A8: A is subcondensed by Def2;
A9: A ` c= Cl (A `) by PRE_TOPC:18;
A10: (Cl (A `)) \/ (Int (A `)) = (Int (A `)) \/ (Fr (A `)) by XBOOLE_1:39;
A11: Fr A = Fr (A `) by TOPS_1:29;
(Cl (Int (A `))) /\ (Cl (Int ((A `) `))) c= Cl (Int (A `)) by XBOOLE_1:17;
then A12: (Int (A `)) \/ ((Cl (Int (A `))) /\ (Cl (Int ((A `) `)))) c= (Int (A `)) \/ (Cl (Int (A `))) by XBOOLE_1:13;
A13: Cl (Int (A `)) c= Cl (A `) by PRE_TOPC:19, TOPS_1:16;
A14: Cl (Int (A `)) = Cl ((Cl A) `) by TDLAT_3:3
.= (Int (Cl A)) ` by TDLAT_3:2 ;
A15: (Int (A `)) \/ (Cl (Int (A `))) = Cl (Int (A `)) by PRE_TOPC:18, XBOOLE_1:12;
Int (A `) c= A ` by TOPS_1:16;
then Cl (A `) = (Int (A `)) \/ ((Cl (Int (A `))) /\ (Cl (Int ((A `) `)))) by A5, A9, A11, A10, XBOOLE_1:1, XBOOLE_1:12;
then A16: Cl (A `) = Cl (Int (A `)) by A13, A12, A15, XBOOLE_0:def_10;
Cl (A `) = (Int A) ` by TDLAT_3:2;
then Int A = ((Int (Cl A)) `) ` by A16, A14;
then A is supercondensed by Def1;
hence A is condensed by A8; ::_thesis: verum
end;
definition
let T be TopStruct ;
let A be Subset of T;
func Border A -> Subset of T equals :: ISOMICHI:def 5
Int (Fr A);
coherence
Int (Fr A) is Subset of T ;
end;
:: deftheorem defines Border ISOMICHI:def_5_:_
for T being TopStruct
for A being Subset of T holds Border A = Int (Fr A);
theorem Th21: :: ISOMICHI:21
for T being TopSpace
for A being Subset of T holds
( Border A is regular_open & Border A = (Int (Cl A)) \ (Cl (Int A)) & Border A = (Int (Cl A)) /\ (Int (Cl (A `))) )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( Border A is regular_open & Border A = (Int (Cl A)) \ (Cl (Int A)) & Border A = (Int (Cl A)) /\ (Int (Cl (A `))) )
let A be Subset of T; ::_thesis: ( Border A is regular_open & Border A = (Int (Cl A)) \ (Cl (Int A)) & Border A = (Int (Cl A)) /\ (Int (Cl (A `))) )
Fr A = Cl (Fr A) by PRE_TOPC:22;
hence Border A is regular_open ; ::_thesis: ( Border A = (Int (Cl A)) \ (Cl (Int A)) & Border A = (Int (Cl A)) /\ (Int (Cl (A `))) )
(Int (Cl A)) \ (Cl (Int A)) = (Int (Cl A)) \ (((Cl (Int A)) `) `)
.= (Int (Cl A)) \ ((Int ((Int A) `)) `) by TDLAT_3:3
.= (Int (Cl A)) \ ((Int (Cl (A `))) `) by TDLAT_3:2
.= (Int (Cl A)) /\ (((Int (Cl (A `))) `) `) by SUBSET_1:13
.= Int ((Cl A) /\ (Cl (A `))) by TOPS_1:17
.= Int (Fr A) by TOPS_1:def_2 ;
hence Border A = (Int (Cl A)) \ (Cl (Int A)) ; ::_thesis: Border A = (Int (Cl A)) /\ (Int (Cl (A `)))
(Int (Cl A)) /\ (Int (Cl (A `))) = Int ((Cl A) /\ (Cl (A `))) by TOPS_1:17
.= Int (Fr A) by TOPS_1:def_2 ;
hence Border A = (Int (Cl A)) /\ (Int (Cl (A `))) ; ::_thesis: verum
end;
registration
let T be TopSpace;
let A be Subset of T;
cluster Border A -> regular_open ;
coherence
Border A is regular_open by Th21;
end;
theorem Th22: :: ISOMICHI:22
for T being TopSpace
for A being Subset of T holds
( A is supercondensed iff ( Int A is regular_open & Border A is empty ) )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is supercondensed iff ( Int A is regular_open & Border A is empty ) )
let A be Subset of T; ::_thesis: ( A is supercondensed iff ( Int A is regular_open & Border A is empty ) )
A1: Int A c= Int (Cl A) by PRE_TOPC:18, TOPS_1:19;
thus ( A is supercondensed implies ( Int A is regular_open & Border A is empty ) ) ::_thesis: ( Int A is regular_open & Border A is empty implies A is supercondensed )
proof
assume A2: A is supercondensed ; ::_thesis: ( Int A is regular_open & Border A is empty )
then Int (Cl A) = Int A by Def1;
then Int (Cl A) c= Cl (Int A) by PRE_TOPC:18;
then (Int (Cl A)) \ (Cl (Int A)) is empty by XBOOLE_1:37;
hence ( Int A is regular_open & Border A is empty ) by A2, Def1, Th21; ::_thesis: verum
end;
assume that
A3: Int A is regular_open and
A4: Border A is empty ; ::_thesis: A is supercondensed
(Int (Cl A)) \ (Cl (Int A)) is empty by A4, Th21;
then Int (Cl A) c= Cl (Int A) by XBOOLE_1:37;
then A5: Int (Int (Cl A)) c= Int (Cl (Int A)) by TOPS_1:19;
Int A = Int (Cl (Int A)) by A3, TOPS_1:def_8;
then Int (Cl A) = Int A by A5, A1, XBOOLE_0:def_10;
hence A is supercondensed by Def1; ::_thesis: verum
end;
theorem Th23: :: ISOMICHI:23
for T being TopSpace
for A being Subset of T holds
( A is subcondensed iff ( Cl A is regular_closed & Border A is empty ) )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is subcondensed iff ( Cl A is regular_closed & Border A is empty ) )
let A be Subset of T; ::_thesis: ( A is subcondensed iff ( Cl A is regular_closed & Border A is empty ) )
A1: Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16;
thus ( A is subcondensed implies ( Cl A is regular_closed & Border A is empty ) ) ::_thesis: ( Cl A is regular_closed & Border A is empty implies A is subcondensed )
proof
assume A2: A is subcondensed ; ::_thesis: ( Cl A is regular_closed & Border A is empty )
then Cl (Int A) = Cl A by Def2;
then Int (Cl A) c= Cl (Int A) by TOPS_1:16;
then (Int (Cl A)) \ (Cl (Int A)) is empty by XBOOLE_1:37;
hence ( Cl A is regular_closed & Border A is empty ) by A2, Def2, Th21; ::_thesis: verum
end;
assume that
A3: Cl A is regular_closed and
A4: Border A is empty ; ::_thesis: A is subcondensed
(Int (Cl A)) \ (Cl (Int A)) is empty by A4, Th21;
then Int (Cl A) c= Cl (Int A) by XBOOLE_1:37;
then A5: Cl (Int (Cl A)) c= Cl (Cl (Int A)) by PRE_TOPC:19;
Cl A = Cl (Int (Cl A)) by A3, TOPS_1:def_7;
then Cl (Int A) = Cl A by A5, A1, XBOOLE_0:def_10;
hence A is subcondensed by Def2; ::_thesis: verum
end;
registration
let T be TopSpace;
let A be Subset of T;
cluster Border (Border A) -> empty ;
coherence
Border (Border A) is empty ;
end;
theorem :: ISOMICHI:24
for T being TopSpace
for A being Subset of T holds
( A is condensed iff ( Int A is regular_open & Cl A is regular_closed & Border A is empty ) )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is condensed iff ( Int A is regular_open & Cl A is regular_closed & Border A is empty ) )
let A be Subset of T; ::_thesis: ( A is condensed iff ( Int A is regular_open & Cl A is regular_closed & Border A is empty ) )
thus ( A is condensed implies ( Int A is regular_open & Cl A is regular_closed & Border A is empty ) ) by Th22, Th23; ::_thesis: ( Int A is regular_open & Cl A is regular_closed & Border A is empty implies A is condensed )
assume that
A1: Int A is regular_open and
A2: Cl A is regular_closed and
A3: Border A is empty ; ::_thesis: A is condensed
A4: A is subcondensed by A2, A3, Th23;
A is supercondensed by A1, A3, Th22;
hence A is condensed by A4; ::_thesis: verum
end;
begin
theorem :: ISOMICHI:25
for A being Subset of R^1
for a being real number st A = ].-infty,a.] holds
Int A = ].-infty,a.[
proof
let A be Subset of R^1; ::_thesis: for a being real number st A = ].-infty,a.] holds
Int A = ].-infty,a.[
let a be real number ; ::_thesis: ( A = ].-infty,a.] implies Int A = ].-infty,a.[ )
assume A = ].-infty,a.] ; ::_thesis: Int A = ].-infty,a.[
then A ` = ].a,+infty.[ by TOPMETR:17, XXREAL_1:224, XXREAL_1:288;
then Cl (A `) = [.a,+infty.[ by BORSUK_5:49;
then (Cl (A `)) ` = ].-infty,a.[ by TOPMETR:17, XXREAL_1:224, XXREAL_1:294;
hence Int A = ].-infty,a.[ by TOPS_1:def_1; ::_thesis: verum
end;
theorem :: ISOMICHI:26
for A being Subset of R^1
for a being real number st A = [.a,+infty.[ holds
Int A = ].a,+infty.[
proof
let A be Subset of R^1; ::_thesis: for a being real number st A = [.a,+infty.[ holds
Int A = ].a,+infty.[
let a be real number ; ::_thesis: ( A = [.a,+infty.[ implies Int A = ].a,+infty.[ )
assume A = [.a,+infty.[ ; ::_thesis: Int A = ].a,+infty.[
then A ` = ].-infty,a.[ by TOPMETR:17, XXREAL_1:224, XXREAL_1:294;
then Cl (A `) = ].-infty,a.] by BORSUK_5:51;
then (Cl (A `)) ` = ].a,+infty.[ by TOPMETR:17, XXREAL_1:224, XXREAL_1:288;
hence Int A = ].a,+infty.[ by TOPS_1:def_1; ::_thesis: verum
end;
theorem Th27: :: ISOMICHI:27
for A being Subset of R^1
for a, b being real number st A = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ holds
Cl A = the carrier of R^1
proof
reconsider B = IRRAT as Subset of R^1 by TOPMETR:17;
let A be Subset of R^1; ::_thesis: for a, b being real number st A = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ holds
Cl A = the carrier of R^1
let a, b be real number ; ::_thesis: ( A = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ implies Cl A = the carrier of R^1 )
assume A1: A = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ ; ::_thesis: Cl A = the carrier of R^1
B c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in A )
assume A2: x in B ; ::_thesis: x in A
then reconsider x9 = x as real number ;
percases ( x9 <= a or ( x9 > a & x9 < b ) or x9 >= b ) ;
suppose x9 <= a ; ::_thesis: x in A
then x9 in ].-infty,a.] by XXREAL_1:234;
then x9 in ].-infty,a.] \/ (IRRAT (a,b)) by XBOOLE_0:def_3;
hence x in A by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose ( x9 > a & x9 < b ) ; ::_thesis: x in A
then x9 in ].a,b.[ by XXREAL_1:4;
then x9 in IRRAT /\ ].a,b.[ by A2, XBOOLE_0:def_4;
then x9 in IRRAT (a,b) by BORSUK_5:def_3;
then x9 in ].-infty,a.] \/ (IRRAT (a,b)) by XBOOLE_0:def_3;
hence x in A by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x9 >= b ; ::_thesis: x in A
then x9 in [.b,+infty.[ by XXREAL_1:236;
hence x in A by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
then A3: Cl B c= Cl A by PRE_TOPC:19;
Cl B = the carrier of R^1 by BORSUK_5:28;
hence Cl A = the carrier of R^1 by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: ISOMICHI:28
for A being Subset of R^1
for a, b being real number st A = RAT (a,b) holds
Int A = {}
proof
let A be Subset of R^1; ::_thesis: for a, b being real number st A = RAT (a,b) holds
Int A = {}
let a, b be real number ; ::_thesis: ( A = RAT (a,b) implies Int A = {} )
assume A1: A = RAT (a,b) ; ::_thesis: Int A = {}
A ` = REAL \ A by TOPMETR:17
.= (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ by A1, BORSUK_5:58 ;
then Cl (A `) = [#] R^1 by Th27;
then (Cl (A `)) ` = {} R^1 by XBOOLE_1:37;
hence Int A = {} by TOPS_1:def_1; ::_thesis: verum
end;
theorem :: ISOMICHI:29
for A being Subset of R^1
for a, b being real number st A = IRRAT (a,b) holds
Int A = {}
proof
reconsider B = IRRAT as Subset of R^1 by TOPMETR:17;
let A be Subset of R^1; ::_thesis: for a, b being real number st A = IRRAT (a,b) holds
Int A = {}
let a, b be real number ; ::_thesis: ( A = IRRAT (a,b) implies Int A = {} )
assume A = IRRAT (a,b) ; ::_thesis: Int A = {}
then A = IRRAT /\ ].a,b.[ by BORSUK_5:def_3;
then A c= B by XBOOLE_1:17;
then A is boundary by TOPGEN_1:54, TOPS_3:11;
hence Int A = {} ; ::_thesis: verum
end;
theorem :: ISOMICHI:30
for a, b being real number st a >= b holds
IRRAT (a,b) = {}
proof
let a, b be real number ; ::_thesis: ( a >= b implies IRRAT (a,b) = {} )
assume A1: a >= b ; ::_thesis: IRRAT (a,b) = {}
IRRAT (a,b) = IRRAT /\ ].a,b.[ by BORSUK_5:def_3
.= IRRAT /\ {} by A1, XXREAL_1:28 ;
hence IRRAT (a,b) = {} ; ::_thesis: verum
end;
theorem Th31: :: ISOMICHI:31
for a, b being real number holds IRRAT (a,b) c= [.a,+infty.[
proof
let a, b be real number ; ::_thesis: IRRAT (a,b) c= [.a,+infty.[
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in IRRAT (a,b) or x in [.a,+infty.[ )
assume A1: x in IRRAT (a,b) ; ::_thesis: x in [.a,+infty.[
then reconsider x = x as real number ;
a < x by A1, BORSUK_5:30;
hence x in [.a,+infty.[ by XXREAL_1:236; ::_thesis: verum
end;
theorem Th32: :: ISOMICHI:32
for A being Subset of R^1
for a, b, c being real number st A = ].-infty,a.[ \/ (RAT (b,c)) & a < b & b < c holds
Int A = ].-infty,a.[
proof
let A be Subset of R^1; ::_thesis: for a, b, c being real number st A = ].-infty,a.[ \/ (RAT (b,c)) & a < b & b < c holds
Int A = ].-infty,a.[
let a, b, c be real number ; ::_thesis: ( A = ].-infty,a.[ \/ (RAT (b,c)) & a < b & b < c implies Int A = ].-infty,a.[ )
reconsider B = [.a,b.], C = IRRAT (b,c), D = [.c,+infty.[ as Subset of R^1 by TOPMETR:17;
assume that
A1: A = ].-infty,a.[ \/ (RAT (b,c)) and
A2: a < b and
A3: b < c ; ::_thesis: Int A = ].-infty,a.[
A4: a < c by A2, A3, XXREAL_0:2;
A ` = REAL \ (].-infty,a.[ \/ (RAT (b,c))) by A1, TOPMETR:17
.= (REAL \ (RAT (b,c))) \ ].-infty,a.[ by XBOOLE_1:41
.= ((].-infty,b.] \/ (IRRAT (b,c))) \/ [.c,+infty.[) \ ].-infty,a.[ by BORSUK_5:58
.= (].-infty,b.] \/ ((IRRAT (b,c)) \/ [.c,+infty.[)) \ ].-infty,a.[ by XBOOLE_1:4
.= (].-infty,b.] \ ].-infty,a.[) \/ (((IRRAT (b,c)) \/ [.c,+infty.[) \ ].-infty,a.[) by XBOOLE_1:42 ;
then A5: A ` = [.a,b.] \/ (((IRRAT (b,c)) \/ [.c,+infty.[) \ ].-infty,a.[) by XXREAL_1:289
.= [.a,b.] \/ (((IRRAT (b,c)) \ ].-infty,a.[) \/ ([.c,+infty.[ \ ].-infty,a.[)) by XBOOLE_1:42 ;
right_closed_halfline c is closed ;
then D is closed by JORDAN5A:23;
then A6: Cl D = D by PRE_TOPC:22;
[.b,+infty.[ misses ].-infty,a.[ by A2, XXREAL_1:94;
then IRRAT (b,c) misses ].-infty,a.[ by Th31, XBOOLE_1:63;
then A7: (IRRAT (b,c)) \ ].-infty,a.[ = IRRAT (b,c) by XBOOLE_1:83;
B is closed by JORDAN5A:23;
then A8: Cl B = B by PRE_TOPC:22;
[.c,+infty.[ misses ].-infty,a.[ by A2, A3, XXREAL_0:2, XXREAL_1:94;
then A ` = [.a,b.] \/ ((IRRAT (b,c)) \/ [.c,+infty.[) by A5, A7, XBOOLE_1:83
.= [.a,b.] \/ ((IRRAT (b,c)) \/ ({c} \/ ].c,+infty.[)) by BORSUK_5:43
.= ([.a,b.] \/ (IRRAT (b,c))) \/ ({c} \/ ].c,+infty.[) by XBOOLE_1:4
.= ([.a,b.] \/ (IRRAT (b,c))) \/ [.c,+infty.[ by BORSUK_5:43 ;
then Cl (A `) = (Cl (B \/ C)) \/ (Cl D) by PRE_TOPC:20
.= ((Cl B) \/ (Cl C)) \/ (Cl D) by PRE_TOPC:20
.= (B \/ [.b,c.]) \/ D by A8, A6, A3, BORSUK_5:32
.= [.a,c.] \/ D by A2, A3, XXREAL_1:165
.= [.a,+infty.[ by A4, BORSUK_5:11 ;
then (Cl (A `)) ` = ].-infty,a.[ by TOPMETR:17, XXREAL_1:224, XXREAL_1:294;
hence Int A = ].-infty,a.[ by TOPS_1:def_1; ::_thesis: verum
end;
Lm1: for a, b being real number st a < b holds
[.a,b.] \/ {b} = [.a,b.]
proof
let a, b be real number ; ::_thesis: ( a < b implies [.a,b.] \/ {b} = [.a,b.] )
assume A1: a < b ; ::_thesis: [.a,b.] \/ {b} = [.a,b.]
then [.a,b.] = [.a,b.[ \/ {b} by XXREAL_1:129
.= ([.a,b.[ \/ {b}) \/ {b} by XBOOLE_1:6 ;
hence [.a,b.] \/ {b} = [.a,b.] by A1, XXREAL_1:129; ::_thesis: verum
end;
theorem :: ISOMICHI:33
for a, b being real number st a < b holds
REAL = (].-infty,a.[ \/ [.a,b.]) \/ ].b,+infty.[
proof
let a, b be real number ; ::_thesis: ( a < b implies REAL = (].-infty,a.[ \/ [.a,b.]) \/ ].b,+infty.[ )
assume A1: a < b ; ::_thesis: REAL = (].-infty,a.[ \/ [.a,b.]) \/ ].b,+infty.[
REAL = (REAL \ {a}) \/ {a} by XBOOLE_1:45
.= (].-infty,a.[ \/ ].a,+infty.[) \/ {a} by XXREAL_1:389
.= ].-infty,a.[ \/ (].a,+infty.[ \/ {a}) by XBOOLE_1:4
.= ].-infty,a.[ \/ [.a,+infty.[ by BORSUK_5:43
.= ].-infty,a.[ \/ ([.a,b.] \/ [.b,+infty.[) by A1, BORSUK_5:11
.= ].-infty,a.[ \/ ([.a,b.] \/ ({b} \/ ].b,+infty.[)) by BORSUK_5:43
.= ].-infty,a.[ \/ (([.a,b.] \/ {b}) \/ ].b,+infty.[) by XBOOLE_1:4
.= (].-infty,a.[ \/ ([.a,b.] \/ {b})) \/ ].b,+infty.[ by XBOOLE_1:4 ;
hence REAL = (].-infty,a.[ \/ [.a,b.]) \/ ].b,+infty.[ by A1, Lm1; ::_thesis: verum
end;
theorem Th34: :: ISOMICHI:34
for A being Subset of R^1
for a, b, c being real number st A = ].-infty,a.] \/ [.b,c.] & a < b & b < c holds
Int A = ].-infty,a.[ \/ ].b,c.[
proof
let A be Subset of R^1; ::_thesis: for a, b, c being real number st A = ].-infty,a.] \/ [.b,c.] & a < b & b < c holds
Int A = ].-infty,a.[ \/ ].b,c.[
let a, b, c be real number ; ::_thesis: ( A = ].-infty,a.] \/ [.b,c.] & a < b & b < c implies Int A = ].-infty,a.[ \/ ].b,c.[ )
assume that
A1: A = ].-infty,a.] \/ [.b,c.] and
A2: a < b and
A3: b < c ; ::_thesis: Int A = ].-infty,a.[ \/ ].b,c.[
a < c by A2, A3, XXREAL_0:2;
then A4: ].c,+infty.[ /\ ].a,+infty.[ = ].c,+infty.[ by XBOOLE_1:28, XXREAL_1:46;
reconsider B = ].a,b.[, C = ].c,+infty.[ as Subset of R^1 by TOPMETR:17;
A5: Cl B = [.a,b.] by A2, BORSUK_5:16;
A6: Cl C = [.c,+infty.[ by BORSUK_5:49;
A ` = REAL \ (].-infty,a.] \/ [.b,c.]) by A1, TOPMETR:17
.= (REAL \ (left_closed_halfline a)) \ [.b,c.] by XBOOLE_1:41
.= (right_open_halfline a) \ [.b,c.] by XXREAL_1:224, XXREAL_1:288
.= ].a,+infty.[ \ ([.b,+infty.[ \ ].c,+infty.[) by XXREAL_1:295
.= (].a,+infty.[ \ [.b,+infty.[) \/ (].a,+infty.[ /\ ].c,+infty.[) by XBOOLE_1:52
.= ].a,b.[ \/ ].c,+infty.[ by A4, XXREAL_1:294 ;
then (Cl (A `)) ` = REAL \ ([.c,+infty.[ \/ [.a,b.]) by A5, A6, PRE_TOPC:20, TOPMETR:17
.= (REAL \ (right_closed_halfline c)) \ [.a,b.] by XBOOLE_1:41
.= (left_open_halfline c) \ [.a,b.] by XXREAL_1:224, XXREAL_1:294
.= ].-infty,a.[ \/ ].b,c.[ by A2, A3, XXREAL_0:2, XXREAL_1:339 ;
hence Int A = ].-infty,a.[ \/ ].b,c.[ by TOPS_1:def_1; ::_thesis: verum
end;
begin
notation
let A, B be set ;
antonym A,B are_c=-incomparable for A,B are_c=-comparable ;
end;
theorem Th35: :: ISOMICHI:35
for A, B being set holds
( A,B are_c=-incomparable or A c= B or B c< A )
proof
let A, B be set ; ::_thesis: ( A,B are_c=-incomparable or A c= B or B c< A )
assume that
A1: A,B are_c=-comparable and
A2: not A c= B and
A3: not B c< A ; ::_thesis: contradiction
( A c= B or B c= A ) by A1, XBOOLE_0:def_9;
hence contradiction by A2, A3, XBOOLE_0:def_8; ::_thesis: verum
end;
definition
let T be TopSpace;
let A be Subset of T;
attrA is 1st_class means :Def6: :: ISOMICHI:def 6
Int (Cl A) c= Cl (Int A);
attrA is 2nd_class means :Def7: :: ISOMICHI:def 7
Cl (Int A) c< Int (Cl A);
attrA is 3rd_class means :Def8: :: ISOMICHI:def 8
Cl (Int A), Int (Cl A) are_c=-incomparable ;
end;
:: deftheorem Def6 defines 1st_class ISOMICHI:def_6_:_
for T being TopSpace
for A being Subset of T holds
( A is 1st_class iff Int (Cl A) c= Cl (Int A) );
:: deftheorem Def7 defines 2nd_class ISOMICHI:def_7_:_
for T being TopSpace
for A being Subset of T holds
( A is 2nd_class iff Cl (Int A) c< Int (Cl A) );
:: deftheorem Def8 defines 3rd_class ISOMICHI:def_8_:_
for T being TopSpace
for A being Subset of T holds
( A is 3rd_class iff Cl (Int A), Int (Cl A) are_c=-incomparable );
theorem :: ISOMICHI:36
for T being TopSpace
for A being Subset of T holds
( A is 1st_class or A is 2nd_class or A is 3rd_class )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is 1st_class or A is 2nd_class or A is 3rd_class )
let A be Subset of T; ::_thesis: ( A is 1st_class or A is 2nd_class or A is 3rd_class )
assume that
A1: not A is 1st_class and
A2: not A is 2nd_class and
A3: not A is 3rd_class ; ::_thesis: contradiction
A4: not Cl (Int A) c< Int (Cl A) by A2, Def7;
A5: Cl (Int A), Int (Cl A) are_c=-comparable by A3, Def8;
not Int (Cl A) c= Cl (Int A) by A1, Def6;
hence contradiction by A4, A5, Th35; ::_thesis: verum
end;
registration
let T be TopSpace;
cluster 1st_class -> non 2nd_class non 3rd_class for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is 1st_class holds
( not b1 is 2nd_class & not b1 is 3rd_class )
proof
let A be Subset of T; ::_thesis: ( A is 1st_class implies ( not A is 2nd_class & not A is 3rd_class ) )
assume A is 1st_class ; ::_thesis: ( not A is 2nd_class & not A is 3rd_class )
then A1: Int (Cl A) c= Cl (Int A) by Def6;
then A2: Cl (Int A), Int (Cl A) are_c=-comparable by XBOOLE_0:def_9;
not Cl (Int A) c< Int (Cl A) by A1, XBOOLE_1:60;
hence ( not A is 2nd_class & not A is 3rd_class ) by A2, Def7, Def8; ::_thesis: verum
end;
cluster 2nd_class -> non 1st_class non 3rd_class for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is 2nd_class holds
( not b1 is 1st_class & not b1 is 3rd_class )
proof
let A be Subset of T; ::_thesis: ( A is 2nd_class implies ( not A is 1st_class & not A is 3rd_class ) )
assume A is 2nd_class ; ::_thesis: ( not A is 1st_class & not A is 3rd_class )
then A3: Cl (Int A) c< Int (Cl A) by Def7;
then Cl (Int A) c= Int (Cl A) by XBOOLE_0:def_8;
then A4: Cl (Int A), Int (Cl A) are_c=-comparable by XBOOLE_0:def_9;
not Int (Cl A) c= Cl (Int A) by A3, XBOOLE_0:def_8;
hence ( not A is 1st_class & not A is 3rd_class ) by A4, Def6, Def8; ::_thesis: verum
end;
cluster 3rd_class -> non 1st_class non 2nd_class for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is 3rd_class holds
( not b1 is 1st_class & not b1 is 2nd_class ) ;
end;
theorem Th37: :: ISOMICHI:37
for T being TopSpace
for A being Subset of T holds
( A is 1st_class iff Border A is empty )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is 1st_class iff Border A is empty )
let A be Subset of T; ::_thesis: ( A is 1st_class iff Border A is empty )
A1: ( Border A is empty implies A is 1st_class )
proof
assume Border A is empty ; ::_thesis: A is 1st_class
then (Int (Cl A)) \ (Cl (Int A)) = {} by Th21;
then Int (Cl A) c= Cl (Int A) by XBOOLE_1:37;
hence A is 1st_class by Def6; ::_thesis: verum
end;
( A is 1st_class implies Border A is empty )
proof
assume A is 1st_class ; ::_thesis: Border A is empty
then Int (Cl A) c= Cl (Int A) by Def6;
then (Int (Cl A)) \ (Cl (Int A)) = {} by XBOOLE_1:37;
hence Border A is empty by Th21; ::_thesis: verum
end;
hence ( A is 1st_class iff Border A is empty ) by A1; ::_thesis: verum
end;
registration
let T be TopSpace;
cluster supercondensed -> 1st_class for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is supercondensed holds
b1 is 1st_class
proof
let A be Subset of T; ::_thesis: ( A is supercondensed implies A is 1st_class )
assume A is supercondensed ; ::_thesis: A is 1st_class
then Border A is empty by Th22;
hence A is 1st_class by Th37; ::_thesis: verum
end;
cluster subcondensed -> 1st_class for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is subcondensed holds
b1 is 1st_class
proof
let A be Subset of T; ::_thesis: ( A is subcondensed implies A is 1st_class )
assume A is subcondensed ; ::_thesis: A is 1st_class
then Border A is empty by Th23;
hence A is 1st_class by Th37; ::_thesis: verum
end;
end;
definition
let T be TopSpace;
attrT is with_1st_class_subsets means :Def9: :: ISOMICHI:def 9
ex A being Subset of T st A is 1st_class ;
attrT is with_2nd_class_subsets means :Def10: :: ISOMICHI:def 10
ex A being Subset of T st A is 2nd_class ;
attrT is with_3rd_class_subsets means :Def11: :: ISOMICHI:def 11
ex A being Subset of T st A is 3rd_class ;
end;
:: deftheorem Def9 defines with_1st_class_subsets ISOMICHI:def_9_:_
for T being TopSpace holds
( T is with_1st_class_subsets iff ex A being Subset of T st A is 1st_class );
:: deftheorem Def10 defines with_2nd_class_subsets ISOMICHI:def_10_:_
for T being TopSpace holds
( T is with_2nd_class_subsets iff ex A being Subset of T st A is 2nd_class );
:: deftheorem Def11 defines with_3rd_class_subsets ISOMICHI:def_11_:_
for T being TopSpace holds
( T is with_3rd_class_subsets iff ex A being Subset of T st A is 3rd_class );
registration
let T be non empty anti-discrete TopSpace;
cluster non empty proper -> 2nd_class for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is proper & not b1 is empty holds
b1 is 2nd_class
proof
let A be Subset of T; ::_thesis: ( A is proper & not A is empty implies A is 2nd_class )
assume A1: ( A is proper & not A is empty ) ; ::_thesis: A is 2nd_class
then A <> the carrier of T by SUBSET_1:def_6;
then Int A = {} by TEX_1:10;
then A2: Cl (Int A) = {} by TEX_1:9;
Cl A = the carrier of T by A1, TEX_1:9;
then Int (Cl A) = the carrier of T by TEX_1:10;
then Cl (Int A) c< Int (Cl A) by A2, XBOOLE_0:def_8;
hence A is 2nd_class by Def7; ::_thesis: verum
end;
end;
registration
let T be non trivial strict anti-discrete TopSpace;
cluster 2nd_class for Element of bool the carrier of T;
existence
ex b1 being Subset of T st b1 is 2nd_class
proof
set x = the Element of T;
reconsider A = { the Element of T} as Subset of T ;
Cl A = the carrier of T by TEX_1:9;
hence ex b1 being Subset of T st b1 is 2nd_class ; ::_thesis: verum
end;
end;
registration
cluster non trivial strict TopSpace-like with_1st_class_subsets with_2nd_class_subsets for TopStruct ;
existence
ex b1 being TopSpace st
( b1 is with_1st_class_subsets & b1 is with_2nd_class_subsets & b1 is strict & not b1 is trivial )
proof
set T = the non trivial strict anti-discrete TopSpace;
set B = the 2nd_class Subset of the non trivial strict anti-discrete TopSpace;
the 2nd_class Subset of the non trivial strict anti-discrete TopSpace is 2nd_class ;
then A1: the non trivial strict anti-discrete TopSpace is with_2nd_class_subsets by Def10;
{} the non trivial strict anti-discrete TopSpace is 1st_class ;
then the non trivial strict anti-discrete TopSpace is with_1st_class_subsets by Def9;
hence ex b1 being TopSpace st
( b1 is with_1st_class_subsets & b1 is with_2nd_class_subsets & b1 is strict & not b1 is trivial ) by A1; ::_thesis: verum
end;
cluster non empty strict TopSpace-like with_3rd_class_subsets for TopStruct ;
existence
ex b1 being TopSpace st
( b1 is with_3rd_class_subsets & not b1 is empty & b1 is strict )
proof
set B = ].-infty,1.[;
set C = RAT (2,4);
take R^1 ; ::_thesis: ( R^1 is with_3rd_class_subsets & not R^1 is empty & R^1 is strict )
set A = ].-infty,1.[ \/ (RAT (2,4));
reconsider A = ].-infty,1.[ \/ (RAT (2,4)), B = ].-infty,1.[, C = RAT (2,4) as Subset of R^1 by TOPMETR:17;
A2: Cl C = [.2,4.] by BORSUK_5:31;
Cl B = ].-infty,1.] by BORSUK_5:51;
then Cl A = ].-infty,1.] \/ [.2,4.] by A2, PRE_TOPC:20;
then A3: Int (Cl A) = ].-infty,1.[ \/ ].2,4.[ by Th34;
A4: Cl (Int A) = ].-infty,1.] by Th32, BORSUK_5:51;
3 in ].2,4.[ by XXREAL_1:4;
then 3 in Int (Cl A) by A3, XBOOLE_0:def_3;
then A5: not Int (Cl A) c= Cl (Int A) by A4, XXREAL_1:234;
A6: not 1 in ].2,4.[ by XXREAL_1:4;
A7: not 1 in ].-infty,1.[ by XXREAL_1:4;
1 in Cl (Int A) by A4, XXREAL_1:234;
then not Cl (Int A) c= Int (Cl A) by A3, A7, A6, XBOOLE_0:def_3;
then Int (Cl A), Cl (Int A) are_c=-incomparable by A5, XBOOLE_0:def_9;
then A is 3rd_class by Def8;
hence ( R^1 is with_3rd_class_subsets & not R^1 is empty & R^1 is strict ) by Def11; ::_thesis: verum
end;
end;
registration
let T be TopSpace;
cluster 1st_class for Element of bool the carrier of T;
existence
ex b1 being Subset of T st b1 is 1st_class
proof
take {} T ; ::_thesis: {} T is 1st_class
thus {} T is 1st_class ; ::_thesis: verum
end;
end;
registration
let T be with_2nd_class_subsets TopSpace;
cluster 2nd_class for Element of bool the carrier of T;
existence
ex b1 being Subset of T st b1 is 2nd_class by Def10;
end;
registration
let T be with_3rd_class_subsets TopSpace;
cluster 3rd_class for Element of bool the carrier of T;
existence
ex b1 being Subset of T st b1 is 3rd_class by Def11;
end;
theorem Th38: :: ISOMICHI:38
for T being TopSpace
for A being Subset of T holds
( A is 1st_class iff A ` is 1st_class )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is 1st_class iff A ` is 1st_class )
let A be Subset of T; ::_thesis: ( A is 1st_class iff A ` is 1st_class )
A1: ( A ` is 1st_class implies A is 1st_class )
proof
assume A ` is 1st_class ; ::_thesis: A is 1st_class
then Int (Cl (A `)) c= Cl (Int (A `)) by Def6;
then Int ((Int A) `) c= Cl (Int (A `)) by TDLAT_3:2;
then (Cl (Int A)) ` c= Cl (Int (A `)) by TDLAT_3:3;
then (Cl (Int A)) ` c= Cl ((Cl A) `) by TDLAT_3:3;
then (Cl (Int A)) ` c= (Int (Cl A)) ` by TDLAT_3:2;
then Int (Cl A) c= Cl (Int A) by SUBSET_1:12;
hence A is 1st_class by Def6; ::_thesis: verum
end;
( A is 1st_class implies A ` is 1st_class )
proof
assume A is 1st_class ; ::_thesis: A ` is 1st_class
then Int (Cl A) c= Cl (Int A) by Def6;
then (Cl (Int A)) ` c= (Int (Cl A)) ` by SUBSET_1:12;
then Int ((Int A) `) c= (Int (Cl A)) ` by TDLAT_3:3;
then Int ((Int A) `) c= Cl ((Cl A) `) by TDLAT_3:2;
then Int ((Int A) `) c= Cl (Int (A `)) by TDLAT_3:3;
then Int (Cl (A `)) c= Cl (Int (A `)) by TDLAT_3:2;
hence A ` is 1st_class by Def6; ::_thesis: verum
end;
hence ( A is 1st_class iff A ` is 1st_class ) by A1; ::_thesis: verum
end;
theorem Th39: :: ISOMICHI:39
for T being TopSpace
for A being Subset of T holds
( A is 2nd_class iff A ` is 2nd_class )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is 2nd_class iff A ` is 2nd_class )
let A be Subset of T; ::_thesis: ( A is 2nd_class iff A ` is 2nd_class )
A1: for A being Subset of T st A ` is 2nd_class holds
A is 2nd_class
proof
let A be Subset of T; ::_thesis: ( A ` is 2nd_class implies A is 2nd_class )
assume A ` is 2nd_class ; ::_thesis: A is 2nd_class
then A2: Cl (Int (A `)) c< Int (Cl (A `)) by Def7;
then Cl (Int (A `)) c= Int (Cl (A `)) by XBOOLE_0:def_8;
then Cl (Int (A `)) c= Int ((Int A) `) by TDLAT_3:2;
then Cl (Int (A `)) c= (Cl (Int A)) ` by TDLAT_3:3;
then Cl ((Cl A) `) c= (Cl (Int A)) ` by TDLAT_3:3;
then (Int (Cl A)) ` c= (Cl (Int A)) ` by TDLAT_3:2;
then A3: Cl (Int A) c= Int (Cl A) by SUBSET_1:12;
Cl ((Cl A) `) <> Int (Cl (A `)) by A2, TDLAT_3:3;
then Cl ((Cl A) `) <> Int ((Int A) `) by TDLAT_3:2;
then (Cl (Int A)) ` <> Cl ((Cl A) `) by TDLAT_3:3;
then Cl (Int A) <> Int (Cl A) by TDLAT_3:2;
then Cl (Int A) c< Int (Cl A) by A3, XBOOLE_0:def_8;
hence A is 2nd_class by Def7; ::_thesis: verum
end;
( A is 2nd_class implies A ` is 2nd_class )
proof
assume A is 2nd_class ; ::_thesis: A ` is 2nd_class
then (A `) ` is 2nd_class ;
hence A ` is 2nd_class by A1; ::_thesis: verum
end;
hence ( A is 2nd_class iff A ` is 2nd_class ) by A1; ::_thesis: verum
end;
theorem Th40: :: ISOMICHI:40
for T being TopSpace
for A being Subset of T holds
( A is 3rd_class iff A ` is 3rd_class )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( A is 3rd_class iff A ` is 3rd_class )
let A be Subset of T; ::_thesis: ( A is 3rd_class iff A ` is 3rd_class )
(Int (Cl A)) ` = Cl ((Cl A) `) by TDLAT_3:2
.= Cl (Int (A `)) by TDLAT_3:3 ;
then A1: Int (Cl A) = (Cl (Int (A `))) ` ;
(Cl (Int A)) ` = Int ((Int A) `) by TDLAT_3:3
.= Int (Cl (A `)) by TDLAT_3:2 ;
then A2: Cl (Int A) = (Int (Cl (A `))) ` ;
A3: ( A ` is 3rd_class implies A is 3rd_class )
proof
assume A ` is 3rd_class ; ::_thesis: A is 3rd_class
then A4: Cl (Int (A `)), Int (Cl (A `)) are_c=-incomparable by Def8;
then not Int (Cl (A `)) c= Cl (Int (A `)) by XBOOLE_0:def_9;
then A5: not Int (Cl A) c= Cl (Int A) by A2, A1, SUBSET_1:12;
not Cl (Int (A `)) c= Int (Cl (A `)) by A4, XBOOLE_0:def_9;
then not Cl (Int A) c= Int (Cl A) by A2, A1, SUBSET_1:12;
then Cl (Int A), Int (Cl A) are_c=-incomparable by A5, XBOOLE_0:def_9;
hence A is 3rd_class by Def8; ::_thesis: verum
end;
( A is 3rd_class implies A ` is 3rd_class )
proof
assume A is 3rd_class ; ::_thesis: A ` is 3rd_class
then A6: Cl (Int A), Int (Cl A) are_c=-incomparable by Def8;
then not Int (Cl A) c= Cl (Int A) by XBOOLE_0:def_9;
then A7: not Int (Cl (A `)) c= Cl (Int (A `)) by A2, A1, SUBSET_1:12;
not Cl (Int A) c= Int (Cl A) by A6, XBOOLE_0:def_9;
then not Cl (Int (A `)) c= Int (Cl (A `)) by A2, A1, SUBSET_1:12;
then Cl (Int (A `)), Int (Cl (A `)) are_c=-incomparable by A7, XBOOLE_0:def_9;
hence A ` is 3rd_class by Def8; ::_thesis: verum
end;
hence ( A is 3rd_class iff A ` is 3rd_class ) by A3; ::_thesis: verum
end;
registration
let T be TopSpace;
let A be 1st_class Subset of T;
clusterA ` -> 1st_class ;
coherence
A ` is 1st_class by Th38;
end;
registration
let T be with_2nd_class_subsets TopSpace;
let A be 2nd_class Subset of T;
clusterA ` -> 2nd_class ;
coherence
A ` is 2nd_class by Th39;
end;
registration
let T be with_3rd_class_subsets TopSpace;
let A be 3rd_class Subset of T;
clusterA ` -> 3rd_class ;
coherence
A ` is 3rd_class by Th40;
end;
theorem Th41: :: ISOMICHI:41
for T being TopSpace
for A being Subset of T st A is 1st_class holds
( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) )
proof
let T be TopSpace; ::_thesis: for A being Subset of T st A is 1st_class holds
( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) )
let A be Subset of T; ::_thesis: ( A is 1st_class implies ( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) ) )
Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16;
then A1: Int (Cl (Int A)) c= Int (Cl A) by TOPS_1:19;
Int A c= Int (Cl A) by PRE_TOPC:18, TOPS_1:19;
then A2: Cl (Int A) c= Cl (Int (Cl A)) by PRE_TOPC:19;
assume A is 1st_class ; ::_thesis: ( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) )
then A3: Int (Cl A) c= Cl (Int A) by Def6;
then A4: Cl (Int (Cl A)) c= Cl (Cl (Int A)) by PRE_TOPC:19;
Int (Int (Cl A)) c= Int (Cl (Int A)) by A3, TOPS_1:19;
hence ( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) ) by A1, A4, A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th42: :: ISOMICHI:42
for T being TopSpace
for A being Subset of T st ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) holds
A is 1st_class
proof
let T be TopSpace; ::_thesis: for A being Subset of T st ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) holds
A is 1st_class
let A be Subset of T; ::_thesis: ( ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) implies A is 1st_class )
assume A1: ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) ; ::_thesis: A is 1st_class
percases ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) by A1;
supposeA2: Int (Cl A) = Int (Cl (Int A)) ; ::_thesis: A is 1st_class
Int (Cl (Int A)) c= Cl (Int A) by TOPS_1:16;
hence A is 1st_class by A2, Def6; ::_thesis: verum
end;
supposeA3: Cl (Int A) = Cl (Int (Cl A)) ; ::_thesis: A is 1st_class
Int (Cl A) c= Cl (Int (Cl A)) by PRE_TOPC:18;
hence A is 1st_class by A3, Def6; ::_thesis: verum
end;
end;
end;
theorem Th43: :: ISOMICHI:43
for T being TopSpace
for A, B being Subset of T st A is 1st_class & B is 1st_class holds
( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) )
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T st A is 1st_class & B is 1st_class holds
( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) )
let A, B be Subset of T; ::_thesis: ( A is 1st_class & B is 1st_class implies ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) ) )
assume that
A1: A is 1st_class and
A2: B is 1st_class ; ::_thesis: ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) )
A3: Cl (Int B) = Cl (Int (Cl B)) by A2, Th41;
Cl (Int A) = Cl (Int (Cl A)) by A1, Th41;
then A4: (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (Cl (A \/ B))) by A3, Th2;
Int (Cl (A /\ B)) c= Int ((Cl A) /\ (Cl B)) by PRE_TOPC:21, TOPS_1:19;
then A5: Int (Cl (A /\ B)) c= (Int (Cl A)) /\ (Int (Cl B)) by TOPS_1:17;
Int (A \/ B) c= Int (Cl (A \/ B)) by PRE_TOPC:18, TOPS_1:19;
then A6: Cl (Int (A \/ B)) c= Cl (Int (Cl (A \/ B))) by PRE_TOPC:19;
Cl ((Int A) \/ (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:19, TOPS_1:20;
then A7: (Cl (Int A)) \/ (Cl (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:20;
A8: Int (Cl B) = Int (Cl (Int B)) by A2, Th41;
Cl (Int (A /\ B)) c= Cl (A /\ B) by PRE_TOPC:19, TOPS_1:16;
then A9: Int (Cl (Int (A /\ B))) c= Int (Cl (A /\ B)) by TOPS_1:19;
Int (Cl A) = Int (Cl (Int A)) by A1, Th41;
then (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (Int (A /\ B))) by A8, Th1;
hence ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) ) by A5, A9, A7, A4, A6, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: ISOMICHI:44
for T being TopSpace
for A, B being Subset of T st A is 1st_class & B is 1st_class holds
( A \/ B is 1st_class & A /\ B is 1st_class )
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T st A is 1st_class & B is 1st_class holds
( A \/ B is 1st_class & A /\ B is 1st_class )
let A, B be Subset of T; ::_thesis: ( A is 1st_class & B is 1st_class implies ( A \/ B is 1st_class & A /\ B is 1st_class ) )
assume that
A1: A is 1st_class and
A2: B is 1st_class ; ::_thesis: ( A \/ B is 1st_class & A /\ B is 1st_class )
A3: Cl (Int A) = Cl (Int (Cl A)) by A1, Th41;
A4: Int (Cl B) = Int (Cl (Int B)) by A2, Th41;
A5: Int (Cl A) = Int (Cl (Int A)) by A1, Th41;
A6: Cl (Int B) = Cl (Int (Cl B)) by A2, Th41;
A7: Cl (Int (A \/ B)) = (Cl (Int A)) \/ (Cl (Int B)) by A1, A2, Th43
.= Cl (Int (Cl (A \/ B))) by A3, A6, Th2 ;
Int (Cl (A /\ B)) = (Int (Cl A)) /\ (Int (Cl B)) by A1, A2, Th43
.= Int (Cl (Int (A /\ B))) by A5, A4, Th1 ;
hence ( A \/ B is 1st_class & A /\ B is 1st_class ) by A7, Th42; ::_thesis: verum
end;