:: by Robert Milewski

::

:: Received June 22, 1999

:: Copyright (c) 1999-2021 Association of Mizar Users

scheme :: YELLOW15:sch 1

SeqLambda1C{ F_{1}() -> Nat, F_{2}() -> non empty set , P_{1}[ object ], F_{3}( object ) -> set , F_{4}( object ) -> set } :

SeqLambda1C{ F

ex p being FinSequence of F_{2}() st

( len p = F_{1}() & ( for i being Nat st i in Seg F_{1}() holds

( ( P_{1}[i] implies p . i = F_{3}(i) ) & ( P_{1}[i] implies p . i = F_{4}(i) ) ) ) )

provided( len p = F

( ( P

A1:
for i being Nat st i in Seg F_{1}() holds

( ( P_{1}[i] implies F_{3}(i) in F_{2}() ) & ( P_{1}[i] implies F_{4}(i) in F_{2}() ) )

( ( P

proof end;

definition

let X be set ;

let p be FinSequence of bool X;

let q be FinSequence of BOOLEAN ;

ex b_{1} being FinSequence of bool X st

( len b_{1} = len p & ( for i being Nat st i in dom p holds

b_{1} . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) )

for b_{1}, b_{2} being FinSequence of bool X st len b_{1} = len p & ( for i being Nat st i in dom p holds

b_{1} . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) & len b_{2} = len p & ( for i being Nat st i in dom p holds

b_{2} . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) holds

b_{1} = b_{2}

end;
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 ( 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))) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{4} being FinSequence of bool X holds

( b_{4} = MergeSequence (p,q) iff ( len b_{4} = len p & ( for i being Nat st i in dom p holds

b_{4} . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) ) );

for X being set

for p being FinSequence of bool X

for q being FinSequence of BOOLEAN

for b

( b

b

::$CT 3

theorem Th1: :: YELLOW15:4

for X being set

for p being FinSequence of bool X

for q being FinSequence of BOOLEAN holds dom (MergeSequence (p,q)) = dom p

for p being FinSequence of bool X

for q being FinSequence of BOOLEAN holds dom (MergeSequence (p,q)) = dom p

proof end;

theorem Th2: :: YELLOW15:5

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

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 Th3: :: YELLOW15:6

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)

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 Th5: :: YELLOW15:8

for X being set

for q being FinSequence of BOOLEAN holds MergeSequence ((<*> (bool X)),q) = <*> (bool X)

for q being FinSequence of BOOLEAN holds MergeSequence ((<*> (bool X)),q) = <*> (bool X)

proof end;

theorem :: YELLOW15:9

for X being set

for x being Subset of X

for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x*>,q)) = 1

for x being Subset of X

for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x*>,q)) = 1

proof end;

theorem :: YELLOW15:10

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

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:11

for X being set

for x, y being Subset of X

for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x,y*>,q)) = 2

for x, y being Subset of X

for q being FinSequence of BOOLEAN holds len (MergeSequence (<*x,y*>,q)) = 2

proof end;

theorem :: YELLOW15:12

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

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:13

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

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:14

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

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 Th12: :: YELLOW15:15

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

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

definition

let X be set ;

let Y be finite Subset-Family of X;

ex b_{1} being Subset-Family of X ex p being FinSequence of bool X st

( len p = card Y & rng p = Y & b_{1} = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } )

for b_{1}, b_{2} being Subset-Family of X st ex p being FinSequence of bool X st

( len p = card Y & rng p = Y & b_{1} = { (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 & b_{2} = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } ) holds

b_{1} = b_{2}

end;
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 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 } );

ex b

( len p = card Y & rng p = Y & b

proof end;

uniqueness for b

( len p = card Y & rng p = Y & b

( len p = card Y & rng p = Y & b

b

proof end;

:: deftheorem Def2 defines Components YELLOW15:def 2 :

for X being set

for Y being finite Subset-Family of X

for b_{3} being Subset-Family of X holds

( b_{3} = Components Y iff ex p being FinSequence of bool X st

( len p = card Y & rng p = Y & b_{3} = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } ) );

for X being set

for Y being finite Subset-Family of X

for b

( b

( len p = card Y & rng p = Y & b

registration
end;

theorem :: YELLOW15:17

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

for Y, Z being finite Subset-Family of X st Z c= Y holds

Components Y is_finer_than Components Z

proof end;

theorem Th16: :: YELLOW15:19

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

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;

:: deftheorem 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 );

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:20

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

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

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

for Y being finite Subset-Family of X st Y is in_general_position holds

Components Y is a_partition of X

proof end;

registration

let L be non empty RelStr ;

coherence

( [#] L is infs-closed & [#] L is sups-closed & [#] L is with_bottom & [#] L is with_top ) by Th20, Th21;

end;
coherence

( [#] L is infs-closed & [#] L is sups-closed & [#] L is with_bottom & [#] L is with_top ) by Th20, Th21;

theorem :: YELLOW15:26

for L being non empty up-complete Poset st L is finite holds

the carrier of L = the carrier of (CompactSublatt L)

the carrier of L = the carrier of (CompactSublatt L)

proof end;

theorem :: YELLOW15:27

for L being lower-bounded sup-Semilattice

for B being Subset of L st B is infinite holds

card B = card (finsups B)

for B being Subset of L st B is infinite holds

card B = card (finsups B)

proof end;

theorem Th26: :: YELLOW15:29

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 )

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

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

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;