begin
scheme
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() ) )
theorem
canceled;
theorem Th2:
theorem
theorem Th4:
begin
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:
(
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 :
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:
theorem Th6:
theorem Th7:
theorem
theorem Th9:
theorem
theorem
theorem
theorem
theorem
theorem
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:
:: 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 } ) );
theorem Th17:
theorem
theorem Th19:
theorem Th20:
:: 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
theorem
theorem
begin
theorem Th24:
theorem Th25:
theorem
theorem
theorem
theorem
theorem Th30:
theorem
theorem