:: Components and Basis of Topological Spaces
:: by Robert Milewski
::
:: Received June 22, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem :: YELLOW15:1
canceled;
theorem Th2: :: YELLOW15:2
theorem :: YELLOW15:3
theorem Th4: :: YELLOW15:4
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)) ) )
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
end;
:: deftheorem Def1 defines MergeSequence YELLOW15:def 1 :
theorem Th5: :: YELLOW15:5
theorem Th6: :: YELLOW15:6
theorem Th7: :: YELLOW15:7
theorem :: YELLOW15:8
theorem Th9: :: YELLOW15:9
theorem :: YELLOW15:10
theorem :: YELLOW15:11
theorem :: YELLOW15:12
theorem :: YELLOW15:13
theorem :: YELLOW15:14
theorem :: YELLOW15:15
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 ) )
theorem Th16: :: YELLOW15:16
:: deftheorem Def2 defines Components YELLOW15:def 2 :
theorem Th17: :: YELLOW15:17
theorem :: YELLOW15:18
theorem Th19: :: YELLOW15:19
theorem Th20: :: YELLOW15:20
:: deftheorem Def3 defines in_general_position YELLOW15:def 3 :
theorem :: YELLOW15:21
theorem :: YELLOW15:22
theorem :: YELLOW15:23
theorem Th24: :: YELLOW15:24
theorem Th25: :: YELLOW15:25
theorem :: YELLOW15:26
theorem :: YELLOW15:27
theorem :: YELLOW15:28
theorem :: YELLOW15:29
theorem Th30: :: YELLOW15:30
theorem :: YELLOW15:31
theorem :: YELLOW15:32