:: YELLOW15 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

definition
let X be set ;
let p be FinSequence of bool X;
:: original: rng
redefine func rng p -> Subset-Family of X;
coherence
rng p is Subset-Family of X
by FINSEQ_1:def 4;
end;

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

theorem :: YELLOW15:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: YELLOW15:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for D being finite set holds i -tuples_on D is finite
proof end;

theorem Th3: :: YELLOW15:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being finite set
for S being Subset-Family of T holds S is finite
proof end;

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

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

theorem Th4: :: YELLOW15:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non trivial set
for x being Element of X ex y being set st
( y in X & x <> y )
proof end;

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 :Def1: :: YELLOW15:def 1
( len it = len p & ( for i being Nat st i in dom p holds
it . i = IFEQ (q . i),TRUE ,(p . i),(X \ (p . i)) ) );
existence
ex b1 being FinSequence of bool X st
( len b1 = len p & ( for i being Nat st i in dom p holds
b1 . i = IFEQ (q . i),TRUE ,(p . i),(X \ (p . i)) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of bool X st len b1 = len p & ( for i being Nat st i in dom p holds
b1 . i = IFEQ (q . i),TRUE ,(p . i),(X \ (p . i)) ) & len b2 = len p & ( for i being Nat st i in dom p holds
b2 . i = IFEQ (q . i),TRUE ,(p . i),(X \ (p . i)) ) holds
b1 = b2
proof end;
end;

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

theorem Th5: :: YELLOW15:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for p being FinSequence of bool X
for q being FinSequence of BOOLEAN holds dom (MergeSequence p,q) = dom p
proof end;

theorem Th6: :: YELLOW15:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for p being FinSequence of bool X
for q being FinSequence of BOOLEAN
for i being Nat st q . i = TRUE holds
(MergeSequence p,q) . i = p . i
proof end;

theorem Th7: :: YELLOW15:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for p being FinSequence of bool X
for q being FinSequence of BOOLEAN
for i being Nat st i in dom p & q . i = FALSE holds
(MergeSequence p,q) . i = X \ (p . i)
proof end;

theorem :: YELLOW15:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for q being FinSequence of BOOLEAN holds len (MergeSequence (<*> (bool X)),q) = 0
proof end;

theorem Th9: :: YELLOW15:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for q being FinSequence of BOOLEAN holds MergeSequence (<*> (bool X)),q = <*> (bool X)
proof end;

theorem :: YELLOW15:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for x being Subset of X
for q being FinSequence of BOOLEAN holds len (MergeSequence <*x*>,q) = 1
proof end;

theorem :: YELLOW15:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for x being Subset of X
for q being FinSequence of BOOLEAN holds
( ( q . 1 = TRUE implies (MergeSequence <*x*>,q) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence <*x*>,q) . 1 = X \ x ) )
proof end;

theorem :: YELLOW15:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for x, y being Subset of X
for q being FinSequence of BOOLEAN holds len (MergeSequence <*x,y*>,q) = 2
proof end;

theorem :: YELLOW15:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for x, y being Subset of X
for q being 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 ) )
proof end;

theorem :: YELLOW15:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for x, y, z being Subset of X
for q being FinSequence of BOOLEAN holds len (MergeSequence <*x,y,z*>,q) = 3
proof end;

theorem :: YELLOW15:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for x, y, z being Subset of X
for q being 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 ) )
proof end;

theorem Th16: :: YELLOW15:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for p being 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
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 X be set ;
let Y be finite Subset-Family of X;
func Components Y -> Subset-Family of X means :Def2: :: YELLOW15:def 2
ex p being 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 } );
existence
ex b1 being Subset-Family of X ex p being FinSequence of bool X st
( len p = card Y & rng p = Y & b1 = { (Intersect (rng (MergeSequence p,q))) where q is FinSequence of BOOLEAN : len q = len p } )
proof end;
uniqueness
for b1, b2 being Subset-Family of X st ex p being FinSequence of bool X st
( len p = card Y & rng p = Y & b1 = { (Intersect (rng (MergeSequence p,q))) where q is FinSequence of BOOLEAN : len q = len p } ) & ex p being FinSequence of bool X st
( len p = card Y & rng p = Y & b2 = { (Intersect (rng (MergeSequence p,q))) where q is FinSequence of BOOLEAN : len q = len p } ) holds
b1 = b2
proof end;
end;

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

registration
let X be set ;
let Y be finite Subset-Family of X;
cluster Components Y -> finite ;
coherence
Components Y is finite
proof end;
end;

theorem Th17: :: YELLOW15:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for Y being empty Subset-Family of X holds Components Y = {X}
proof end;

theorem :: YELLOW15:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for Y, Z being finite Subset-Family of X st Z c= Y holds
Components Y is_finer_than Components Z
proof end;

theorem Th19: :: YELLOW15:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for Y being finite Subset-Family of X holds union (Components Y) = X
proof end;

theorem Th20: :: YELLOW15:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for Y being finite Subset-Family of X
for A, B being set st A in Components Y & B in Components Y & A <> B holds
A misses B
proof end;

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

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

theorem :: YELLOW15:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for Y, Z being finite Subset-Family of X st Z is in_general_position & Y c= Z holds
Y is in_general_position
proof end;

theorem :: YELLOW15:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being empty Subset-Family of X holds Y is in_general_position
proof end;

theorem :: YELLOW15:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being finite Subset-Family of X st Y is in_general_position holds
Components Y is a_partition of X
proof end;

theorem Th24: :: YELLOW15:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr holds
( [#] L is infs-closed & [#] L is sups-closed )
proof end;

theorem Th25: :: YELLOW15:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr holds
( [#] L is with_bottom & [#] L is with_top )
proof end;

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

theorem :: YELLOW15:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being continuous sup-Semilattice holds [#] L is CLbasis of L
proof end;

theorem :: YELLOW15:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty up-complete Poset st L is finite holds
the carrier of L = the carrier of (CompactSublatt L)
proof end;

theorem :: YELLOW15:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded sup-Semilattice
for B being Subset of L st not B is finite holds
Card B = Card (finsups B)
proof end;

theorem :: YELLOW15:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty T_0 TopSpace holds Card the carrier of T c= Card the topology of T
proof end;

theorem Th30: :: YELLOW15:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopStruct
for X being Subset of T st X is open holds
for B being finite Subset-Family of T st B is Basis of T holds
for Y being set holds
( not Y in Components B or X misses Y or Y c= X )
proof end;

theorem :: YELLOW15:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being T_0 TopSpace st not T is finite holds
for B being Basis of T holds not B is finite
proof end;

theorem :: YELLOW15:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace st T is finite holds
for B being Basis of T
for x being Element of T holds meet { A where A is Element of the topology of T : x in A } in B
proof end;