:: Components and Basis of Topological Spaces
:: by Robert Milewski
::
:: Received June 22, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, XBOOLE_0, FINSEQ_1, FUNCT_1, RELAT_1, TARSKI,
SUBSET_1, MARGREL1, FINSET_1, FINSEQ_2, CARD_1, SETFAM_1, STRUCT_0,
ZFMISC_1, FUNCOP_1, XBOOLEAN, EQREL_1, ORDERS_2, WAYBEL23, YELLOW_0,
LATTICES, ORDINAL2, WAYBEL_0, WAYBEL_3, WAYBEL_8, RCOMP_1, PRE_TOPC,
RLVECT_3, CANTOR_1, YELLOW15;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, SETFAM_1, DOMAIN_1,
CARD_1, NUMBERS, FINSET_1, STRUCT_0, MARGREL1, RELAT_1, FUNCT_1,
RELSET_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, EQREL_1, FUNCOP_1,
CARD_3, PRE_TOPC, TOPS_2, CANTOR_1, ORDERS_2, YELLOW_0, WAYBEL_0,
WAYBEL_3, WAYBEL_8, WAYBEL23;
constructors XXREAL_0, FINSEQ_4, REALSET1, VALUAT_1, TOPS_2, CANTOR_1,
WAYBEL_8, WAYBEL23, RELSET_1, NUMBERS;
registrations SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, FINSEQ_1, MARGREL1,
FINSEQ_2, STRUCT_0, TOPS_1, LATTICE3, WAYBEL_0, WAYBEL_3, WAYBEL23,
ORDINAL1, PRE_TOPC, ZFMISC_1, CARD_1, RELAT_1, FINSEQ_3;
requirements NUMERALS, REAL, SUBSET, BOOLE;
begin :: Preliminaries
scheme :: YELLOW15:sch 1
SeqLambda1C{ i() -> Nat, D() -> non empty set, C[object],
F, G(object)->set } :
ex p be FinSequence of D() st len p = i() & for i be Nat st i in Seg i(
) holds (C[i] implies p.i = F(i)) & (not C[i] implies p.i = G(i))
provided
for i be Nat st i in Seg i() holds (C[i] implies F(i) in D()) & (not
C[i] implies G(i) in D());
begin :: Components
definition
let X be set;
let p be FinSequence of bool X;
let q be FinSequence of BOOLEAN;
func MergeSequence(p,q) -> FinSequence of bool X means
:: YELLOW15:def 1
len it = len p
& for i be Nat st i in dom p holds it.i = IFEQ(q.i,TRUE,p.i,X\p.i);
end;
::$CT 3
theorem :: YELLOW15:4
for X be set for p be FinSequence of bool X for q be FinSequence
of BOOLEAN holds dom MergeSequence(p,q) = dom p;
theorem :: YELLOW15:5
for X be set for p be FinSequence of bool X for q be FinSequence
of BOOLEAN for i be Nat st q.i = TRUE holds MergeSequence(p,q).i = p.i;
theorem :: YELLOW15:6
for X be set for p be FinSequence of bool X for q be FinSequence
of BOOLEAN for i be Nat st i in dom p & q.i = FALSE holds MergeSequence(p,q).i
= X\p.i;
theorem :: YELLOW15:7
for X be set for q be FinSequence of BOOLEAN holds len MergeSequence(
<*>(bool X),q) = 0;
theorem :: YELLOW15:8
for X be set for q be FinSequence of BOOLEAN holds MergeSequence(
<*>(bool X),q) = <*>(bool X);
theorem :: YELLOW15:9
for X be set for x be Subset of X for q be FinSequence of BOOLEAN
holds len MergeSequence(<*x*>,q) = 1;
theorem :: YELLOW15:10
for X be set for x be Subset of X for q be FinSequence of BOOLEAN
holds (q.1 = TRUE implies MergeSequence(<*x*>,q).1 = x) & (q.1 = FALSE implies
MergeSequence(<*x*>,q).1 = X\x);
theorem :: YELLOW15:11
for X be set for x,y be Subset of X for q be FinSequence of BOOLEAN
holds len MergeSequence(<*x,y*>,q) = 2;
theorem :: YELLOW15:12
for X be set for x,y be Subset of X for q be FinSequence of BOOLEAN
holds (q.1 = TRUE implies MergeSequence(<*x,y*>,q).1 = x) & (q.1 = FALSE
implies MergeSequence(<*x,y*>,q).1 = X\x) & (q.2 = TRUE implies MergeSequence(
<*x,y*>,q).2 = y) & (q.2 = FALSE implies MergeSequence(<*x,y*>,q).2 = X\y);
theorem :: YELLOW15:13
for X be set for x,y,z be Subset of X for q be FinSequence of BOOLEAN
holds len MergeSequence(<*x,y,z*>,q) = 3;
theorem :: YELLOW15:14
for X be set for x,y,z be Subset of X for q be FinSequence of BOOLEAN
holds (q.1 = TRUE implies MergeSequence(<*x,y,z*>,q).1 = x) & (q.1 = FALSE
implies MergeSequence(<*x,y,z*>,q).1 = X\x) & (q.2 = TRUE implies MergeSequence
(<*x,y,z*>,q).2 = y) & (q.2 = FALSE implies MergeSequence(<*x,y,z*>,q).2 = X\y)
& (q.3 = TRUE implies MergeSequence(<*x,y,z*>,q).3 = z) & (q.3 = FALSE implies
MergeSequence(<*x,y,z*>,q).3 = X\z);
theorem :: YELLOW15:15
for X be set for p be FinSequence of bool X holds { Intersect (
rng MergeSequence(p,q)) where q is FinSequence of BOOLEAN : len q = len p } is
Subset-Family of X;
registration
cluster -> boolean-valued for FinSequence of BOOLEAN;
end;
definition
let X be set;
let Y be finite Subset-Family of X;
func Components(Y) -> Subset-Family of X means
:: YELLOW15:def 2
ex p be FinSequence of
bool X st len p = card Y & rng p = Y & it = { Intersect (rng MergeSequence(p,q)
) where q is FinSequence of BOOLEAN : len q = len p };
end;
registration
let X be set;
let Y be finite Subset-Family of X;
cluster Components(Y) -> finite;
end;
theorem :: YELLOW15:16
for X be set for Y be empty Subset-Family of X holds Components( Y) = {X};
theorem :: YELLOW15:17
for X be set for Y,Z be finite Subset-Family of X st Z c= Y holds
Components(Y) is_finer_than Components(Z);
theorem :: YELLOW15:18
for X be set for Y be finite Subset-Family of X holds union Components(Y) = X
;
theorem :: YELLOW15:19
for X be set for Y be finite Subset-Family of X for A,B be set
st A in Components(Y) & B in Components(Y) & A <> B holds A misses B;
definition
let X be set;
let Y be finite Subset-Family of X;
attr Y is in_general_position means
:: YELLOW15:def 3
not {} in Components(Y);
end;
theorem :: YELLOW15:20
for X be set for Y,Z be finite Subset-Family of X st Z is
in_general_position & Y c= Z holds Y is in_general_position;
theorem :: YELLOW15:21
for X be non empty set for Y be empty Subset-Family of X holds Y is
in_general_position;
theorem :: YELLOW15:22
for X be non empty set for Y be finite Subset-Family of X st Y is
in_general_position holds Components(Y) is a_partition of X;
begin :: About basis of Topological Spaces
theorem :: YELLOW15:23
for L be non empty RelStr holds [#]L is infs-closed sups-closed;
theorem :: YELLOW15:24
for L be non empty RelStr holds [#]L is with_bottom with_top;
registration
let L be non empty RelStr;
cluster [#]L -> infs-closed sups-closed with_bottom with_top;
end;
theorem :: YELLOW15:25
for L be continuous sup-Semilattice holds [#]L is CLbasis of L;
theorem :: YELLOW15:26
for L be up-complete non empty Poset st L is finite holds the
carrier of L = the carrier of CompactSublatt L;
theorem :: YELLOW15:27
for L be lower-bounded sup-Semilattice for B be Subset of L st B is
infinite holds card B = card finsups B;
theorem :: YELLOW15:28
for T be T_0 non empty TopSpace holds card the carrier of T c= card
the topology of T;
theorem :: YELLOW15:29
for T be TopStruct for X be Subset of T st X is open for B be
finite Subset-Family of T st B is Basis of T for Y be set st Y in Components(B)
holds X misses Y or Y c= X;
theorem :: YELLOW15:30
for T be T_0 TopSpace st T is infinite for B be Basis of T holds B is
infinite;
theorem :: YELLOW15:31
for T be non empty TopSpace st T is finite for B be Basis of T for x
be Element of T holds meet { A where A is Element of the topology of T : x in A
} in B;