:: YELLOW15 semantic presentation

scheme :: YELLOW15:sch 1
s1{ F1() -> Nat, F2() -> non empty set , P1[ set ], F3( set ) -> set , F4( set ) -> set } :
ex b1 being FinSequence of F2() st
( len b1 = F1() & ( for b2 being Nat st b2 in Seg F1() holds
( ( P1[b2] implies b1 . b2 = F3(b2) ) & ( P1[b2] implies b1 . b2 = F4(b2) ) ) ) )
provided
E1: for b1 being Nat st b1 in Seg F1() holds
( ( P1[b1] implies F3(b1) in F2() ) & ( P1[b1] implies F4(b1) in F2() ) )
proof end;

definition
let c1 be set ;
let c2 be FinSequence of bool c1;
redefine func rng as rng c2 -> Subset-Family of a1;
coherence
rng c2 is Subset-Family of c1 by FINSEQ_1:def 4;
end;

registration
cluster BOOLEAN -> finite ;
coherence
BOOLEAN is finite by MARGREL1:def 12;
end;

theorem Th1: :: YELLOW15:1
canceled;

theorem Th2: :: YELLOW15:2
for b1 being Nat
for b2 being finite set holds b1 -tuples_on b2 is finite
proof end;

theorem Th3: :: YELLOW15:3
for b1 being finite set
for b2 being Subset-Family of b1 holds b2 is finite
proof end;

registration
let c1 be finite set ;
cluster -> finite Element of bool (bool a1);
coherence
for b1 being Subset-Family of c1 holds b1 is finite by Th3;
end;

registration
let c1 be finite 1-sorted ;
cluster -> finite Element of bool (bool the carrier of a1);
coherence
for b1 being Subset-Family of c1 holds b1 is finite
proof end;
end;

theorem Th4: :: YELLOW15:4
for b1 being non trivial set
for b2 being Element of b1 ex b3 being set st
( b3 in b1 & b2 <> b3 )
proof end;

definition
let c1 be set ;
let c2 be FinSequence of bool c1;
let c3 be FinSequence of BOOLEAN ;
func MergeSequence c2,c3 -> FinSequence of bool a1 means :Def1: :: YELLOW15:def 1
( len a4 = len a2 & ( for b1 being Nat st b1 in dom a2 holds
a4 . b1 = IFEQ (a3 . b1),TRUE ,(a2 . b1),(a1 \ (a2 . b1)) ) );
existence
ex b1 being FinSequence of bool c1 st
( len b1 = len c2 & ( for b2 being Nat st b2 in dom c2 holds
b1 . b2 = IFEQ (c3 . b2),TRUE ,(c2 . b2),(c1 \ (c2 . b2)) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of bool c1 st len b1 = len c2 & ( for b3 being Nat st b3 in dom c2 holds
b1 . b3 = IFEQ (c3 . b3),TRUE ,(c2 . b3),(c1 \ (c2 . b3)) ) & len b2 = len c2 & ( for b3 being Nat st b3 in dom c2 holds
b2 . b3 = IFEQ (c3 . b3),TRUE ,(c2 . b3),(c1 \ (c2 . b3)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines MergeSequence YELLOW15:def 1 :
for b1 being set
for b2 being FinSequence of bool b1
for b3 being FinSequence of BOOLEAN
for b4 being FinSequence of bool b1 holds
( b4 = MergeSequence b2,b3 iff ( len b4 = len b2 & ( for b5 being Nat st b5 in dom b2 holds
b4 . b5 = IFEQ (b3 . b5),TRUE ,(b2 . b5),(b1 \ (b2 . b5)) ) ) );

theorem Th5: :: YELLOW15:5
for b1 being set
for b2 being FinSequence of bool b1
for b3 being FinSequence of BOOLEAN holds dom (MergeSequence b2,b3) = dom b2
proof end;

theorem Th6: :: YELLOW15:6
for b1 being set
for b2 being FinSequence of bool b1
for b3 being FinSequence of BOOLEAN
for b4 being Nat st b3 . b4 = TRUE holds
(MergeSequence b2,b3) . b4 = b2 . b4
proof end;

theorem Th7: :: YELLOW15:7
for b1 being set
for b2 being FinSequence of bool b1
for b3 being FinSequence of BOOLEAN
for b4 being Nat st b4 in dom b2 & b3 . b4 = FALSE holds
(MergeSequence b2,b3) . b4 = b1 \ (b2 . b4)
proof end;

theorem Th8: :: YELLOW15:8
for b1 being set
for b2 being FinSequence of BOOLEAN holds len (MergeSequence (<*> (bool b1)),b2) = 0
proof end;

theorem Th9: :: YELLOW15:9
for b1 being set
for b2 being FinSequence of BOOLEAN holds MergeSequence (<*> (bool b1)),b2 = <*> (bool b1)
proof end;

theorem Th10: :: YELLOW15:10
for b1 being set
for b2 being Subset of b1
for b3 being FinSequence of BOOLEAN holds len (MergeSequence <*b2*>,b3) = 1
proof end;

theorem Th11: :: YELLOW15:11
for b1 being set
for b2 being Subset of b1
for b3 being FinSequence of BOOLEAN holds
( ( b3 . 1 = TRUE implies (MergeSequence <*b2*>,b3) . 1 = b2 ) & ( b3 . 1 = FALSE implies (MergeSequence <*b2*>,b3) . 1 = b1 \ b2 ) )
proof end;

theorem Th12: :: YELLOW15:12
for b1 being set
for b2, b3 being Subset of b1
for b4 being FinSequence of BOOLEAN holds len (MergeSequence <*b2,b3*>,b4) = 2
proof end;

theorem Th13: :: YELLOW15:13
for b1 being set
for b2, b3 being Subset of b1
for b4 being FinSequence of BOOLEAN holds
( ( b4 . 1 = TRUE implies (MergeSequence <*b2,b3*>,b4) . 1 = b2 ) & ( b4 . 1 = FALSE implies (MergeSequence <*b2,b3*>,b4) . 1 = b1 \ b2 ) & ( b4 . 2 = TRUE implies (MergeSequence <*b2,b3*>,b4) . 2 = b3 ) & ( b4 . 2 = FALSE implies (MergeSequence <*b2,b3*>,b4) . 2 = b1 \ b3 ) )
proof end;

theorem Th14: :: YELLOW15:14
for b1 being set
for b2, b3, b4 being Subset of b1
for b5 being FinSequence of BOOLEAN holds len (MergeSequence <*b2,b3,b4*>,b5) = 3
proof end;

theorem Th15: :: YELLOW15:15
for b1 being set
for b2, b3, b4 being Subset of b1
for b5 being FinSequence of BOOLEAN holds
( ( b5 . 1 = TRUE implies (MergeSequence <*b2,b3,b4*>,b5) . 1 = b2 ) & ( b5 . 1 = FALSE implies (MergeSequence <*b2,b3,b4*>,b5) . 1 = b1 \ b2 ) & ( b5 . 2 = TRUE implies (MergeSequence <*b2,b3,b4*>,b5) . 2 = b3 ) & ( b5 . 2 = FALSE implies (MergeSequence <*b2,b3,b4*>,b5) . 2 = b1 \ b3 ) & ( b5 . 3 = TRUE implies (MergeSequence <*b2,b3,b4*>,b5) . 3 = b4 ) & ( b5 . 3 = FALSE implies (MergeSequence <*b2,b3,b4*>,b5) . 3 = b1 \ b4 ) )
proof end;

theorem Th16: :: YELLOW15:16
for b1 being set
for b2 being FinSequence of bool b1 holds { (Intersect (rng (MergeSequence b2,b3))) where B is FinSequence of BOOLEAN : len b3 = len b2 } is Subset-Family of b1
proof end;

registration
cluster -> boolean-valued FinSequence of BOOLEAN ;
coherence
for b1 being FinSequence of BOOLEAN holds b1 is boolean-valued
proof end;
end;

definition
let c1 be set ;
let c2 be finite Subset-Family of c1;
func Components c2 -> Subset-Family of a1 means :Def2: :: YELLOW15:def 2
ex b1 being FinSequence of bool a1 st
( len b1 = card a2 & rng b1 = a2 & a3 = { (Intersect (rng (MergeSequence b1,b2))) where B is FinSequence of BOOLEAN : len b2 = len b1 } );
existence
ex b1 being Subset-Family of c1ex b2 being FinSequence of bool c1 st
( len b2 = card c2 & rng b2 = c2 & b1 = { (Intersect (rng (MergeSequence b2,b3))) where B is FinSequence of BOOLEAN : len b3 = len b2 } )
proof end;
uniqueness
for b1, b2 being Subset-Family of c1 st ex b3 being FinSequence of bool c1 st
( len b3 = card c2 & rng b3 = c2 & b1 = { (Intersect (rng (MergeSequence b3,b4))) where B is FinSequence of BOOLEAN : len b4 = len b3 } ) & ex b3 being FinSequence of bool c1 st
( len b3 = card c2 & rng b3 = c2 & b2 = { (Intersect (rng (MergeSequence b3,b4))) where B is FinSequence of BOOLEAN : len b4 = len b3 } ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Components YELLOW15:def 2 :
for b1 being set
for b2 being finite Subset-Family of b1
for b3 being Subset-Family of b1 holds
( b3 = Components b2 iff ex b4 being FinSequence of bool b1 st
( len b4 = card b2 & rng b4 = b2 & b3 = { (Intersect (rng (MergeSequence b4,b5))) where B is FinSequence of BOOLEAN : len b5 = len b4 } ) );

registration
let c1 be set ;
let c2 be finite Subset-Family of c1;
cluster Components a2 -> finite ;
coherence
Components c2 is finite
proof end;
end;

theorem Th17: :: YELLOW15:17
for b1 being set
for b2 being empty Subset-Family of b1 holds Components b2 = {b1}
proof end;

theorem Th18: :: YELLOW15:18
for b1 being set
for b2, b3 being finite Subset-Family of b1 st b3 c= b2 holds
Components b2 is_finer_than Components b3
proof end;

theorem Th19: :: YELLOW15:19
for b1 being set
for b2 being finite Subset-Family of b1 holds union (Components b2) = b1
proof end;

theorem Th20: :: YELLOW15:20
for b1 being set
for b2 being finite Subset-Family of b1
for b3, b4 being set st b3 in Components b2 & b4 in Components b2 & b3 <> b4 holds
b3 misses b4
proof end;

definition
let c1 be set ;
let c2 be finite Subset-Family of c1;
attr a2 is in_general_position means :Def3: :: YELLOW15:def 3
not {} in Components a2;
end;

:: deftheorem Def3 defines in_general_position YELLOW15:def 3 :
for b1 being set
for b2 being finite Subset-Family of b1 holds
( b2 is in_general_position iff not {} in Components b2 );

theorem Th21: :: YELLOW15:21
for b1 being set
for b2, b3 being finite Subset-Family of b1 st b3 is in_general_position & b2 c= b3 holds
b2 is in_general_position
proof end;

theorem Th22: :: YELLOW15:22
for b1 being non empty set
for b2 being empty Subset-Family of b1 holds b2 is in_general_position
proof end;

theorem Th23: :: YELLOW15:23
for b1 being non empty set
for b2 being finite Subset-Family of b1 st b2 is in_general_position holds
Components b2 is a_partition of b1
proof end;

theorem Th24: :: YELLOW15:24
for b1 being non empty RelStr holds
( [#] b1 is infs-closed & [#] b1 is sups-closed )
proof end;

theorem Th25: :: YELLOW15:25
for b1 being non empty RelStr holds
( [#] b1 is with_bottom & [#] b1 is with_top )
proof end;

registration
let c1 be non empty RelStr ;
cluster [#] a1 -> infs-closed sups-closed with_bottom with_top ;
coherence
( [#] c1 is infs-closed & [#] c1 is sups-closed & [#] c1 is with_bottom & [#] c1 is with_top ) by Th24, Th25;
end;

theorem Th26: :: YELLOW15:26
for b1 being continuous sup-Semilattice holds [#] b1 is CLbasis of b1
proof end;

theorem Th27: :: YELLOW15:27
for b1 being non empty up-complete Poset st b1 is finite holds
the carrier of b1 = the carrier of (CompactSublatt b1)
proof end;

theorem Th28: :: YELLOW15:28
for b1 being lower-bounded sup-Semilattice
for b2 being Subset of b1 st not b2 is finite holds
Card b2 = Card (finsups b2)
proof end;

theorem Th29: :: YELLOW15:29
for b1 being non empty T_0 TopSpace holds Card the carrier of b1 c= Card the topology of b1
proof end;

theorem Th30: :: YELLOW15:30
for b1 being TopStruct
for b2 being Subset of b1 st b2 is open holds
for b3 being finite Subset-Family of b1 st b3 is Basis of b1 holds
for b4 being set holds
( not b4 in Components b3 or b2 misses b4 or b4 c= b2 )
proof end;

theorem Th31: :: YELLOW15:31
for b1 being T_0 TopSpace st not b1 is finite holds
for b2 being Basis of b1 holds not b2 is finite
proof end;

theorem Th32: :: YELLOW15:32
for b1 being non empty TopSpace st b1 is finite holds
for b2 being Basis of b1
for b3 being Element of b1 holds meet { b4 where B is Element of the topology of b1 : b3 in b4 } in b2
proof end;