let X be 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
let Y, Z be finite Subset-Family of X; ( Z is in_general_position & Y c= Z implies Y is in_general_position )
assume that
A1:
Z is in_general_position
and
A2:
Y c= Z
; Y is in_general_position
A3:
not {} in Components Z
by A1;
not {} in Components Y
proof
deffunc H1(
set )
-> Element of
BOOLEAN =
TRUE ;
consider p being
FinSequence of
bool X such that A4:
len p = card Y
and A5:
rng p = Y
and A6:
Components Y = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p }
by Def2;
A7:
p is
one-to-one
by A4, A5, FINSEQ_4:62;
then A8:
rng p = dom (p ")
by FUNCT_1:33;
consider p1 being
FinSequence of
bool X such that A9:
len p1 = card Z
and A10:
rng p1 = Z
and A11:
Components Z = { (Intersect (rng (MergeSequence (p1,q)))) where q is FinSequence of BOOLEAN : len q = len p1 }
by Def2;
defpred S1[
set ]
means p1 . $1
in rng p;
assume
{} in Components Y
;
contradiction
then consider q being
FinSequence of
BOOLEAN such that A12:
{} = Intersect (rng (MergeSequence (p,q)))
and A13:
len q = len p
by A6;
deffunc H2(
set )
-> set =
((q * (p ")) * p1) . $1;
A14:
dom p = rng (p ")
by A7, FUNCT_1:33;
A15:
for
i being
Nat st
i in Seg (len p1) holds
( (
S1[
i] implies
H2(
i)
in BOOLEAN ) & ( not
S1[
i] implies
H1(
i)
in BOOLEAN ) )
proof
let i be
Nat;
( i in Seg (len p1) implies ( ( S1[i] implies H2(i) in BOOLEAN ) & ( not S1[i] implies H1(i) in BOOLEAN ) ) )
assume
i in Seg (len p1)
;
( ( S1[i] implies H2(i) in BOOLEAN ) & ( not S1[i] implies H1(i) in BOOLEAN ) )
then A16:
i in dom p1
by FINSEQ_1:def 3;
thus
(
p1 . i in rng p implies
((q * (p ")) * p1) . i in BOOLEAN )
( not S1[i] implies H1(i) in BOOLEAN )proof
assume A17:
p1 . i in rng p
;
((q * (p ")) * p1) . i in BOOLEAN
rng (p ") = dom q
by A13, A14, FINSEQ_3:29;
then
p1 . i in dom (q * (p "))
by A8, A17, RELAT_1:27;
then A18:
(q * (p ")) . (p1 . i) in rng (q * (p "))
by FUNCT_1:def 3;
dom (q * (p ")) c= rng p
by A8, RELAT_1:25;
then
rng (q * (p ")) = rng ((q * (p ")) * p1)
by A2, A5, A10, RELAT_1:28, XBOOLE_1:1;
then
((q * (p ")) * p1) . i in rng ((q * (p ")) * p1)
by A16, A18, FUNCT_1:13;
hence
((q * (p ")) * p1) . i in BOOLEAN
;
verum
end;
thus
( not
S1[
i] implies
H1(
i)
in BOOLEAN )
;
verum
end;
consider q1 being
FinSequence of
BOOLEAN such that A19:
len q1 = len p1
and A20:
for
i being
Nat st
i in Seg (len p1) holds
( (
S1[
i] implies
q1 . i = H2(
i) ) & ( not
S1[
i] implies
q1 . i = H1(
i) ) )
from YELLOW15:sch 1(A15);
A21:
p1 is
one-to-one
by A9, A10, FINSEQ_4:62;
then A22:
rng p1 = dom (p1 ")
by FUNCT_1:33;
rng (MergeSequence (p,q)) c= rng (MergeSequence (p1,q1))
proof
let z be
object ;
TARSKI:def 3 ( not z in rng (MergeSequence (p,q)) or z in rng (MergeSequence (p1,q1)) )
assume
z in rng (MergeSequence (p,q))
;
z in rng (MergeSequence (p1,q1))
then consider i being
Nat such that A23:
i in dom (MergeSequence (p,q))
and A24:
(MergeSequence (p,q)) . i = z
by FINSEQ_2:10;
i in Seg (len (MergeSequence (p,q)))
by A23, FINSEQ_1:def 3;
then
i in Seg (len p)
by Def1;
then A25:
i in dom p
by FINSEQ_1:def 3;
then A26:
i in dom ((p1 ") * p)
by A2, A5, A10, A22, RELAT_1:27;
then
((p1 ") * p) . i in rng ((p1 ") * p)
by FUNCT_1:def 3;
then A27:
((p1 ") * p) . i in rng (p1 ")
by FUNCT_1:14;
then A28:
((p1 ") * p) . i in dom p1
by A21, FUNCT_1:33;
then reconsider j =
((p1 ") * p) . i as
Element of
NAT ;
p1 . j =
(p1 * ((p1 ") * p)) . i
by A26, FUNCT_1:13
.=
((p1 * (p1 ")) * p) . i
by RELAT_1:36
.=
((id (rng p1)) * p) . i
by A21, FUNCT_1:39
.=
p . i
by A2, A5, A10, RELAT_1:53
;
then A29:
p1 . j in rng p
by A25, FUNCT_1:def 3;
j in Seg (len p1)
by A28, FINSEQ_1:def 3;
then A30:
q1 . j =
((q * (p ")) * p1) . (((p1 ") * p) . i)
by A20, A29
.=
(((q * (p ")) * p1) * ((p1 ") * p)) . i
by A26, FUNCT_1:13
.=
((q * (p ")) * (p1 * ((p1 ") * p))) . i
by RELAT_1:36
.=
((q * (p ")) * ((p1 * (p1 ")) * p)) . i
by RELAT_1:36
.=
((q * (p ")) * ((id (rng p1)) * p)) . i
by A21, FUNCT_1:39
.=
((q * (p ")) * p) . i
by A2, A5, A10, RELAT_1:53
.=
(q * ((p ") * p)) . i
by RELAT_1:36
.=
(q * (id (dom p))) . i
by A7, FUNCT_1:39
.=
(q * (id (dom q))) . i
by A13, FINSEQ_3:29
.=
q . i
by RELAT_1:52
;
A31:
j in dom p1
by A21, A27, FUNCT_1:33;
A32:
now z = (MergeSequence (p1,q1)) . jper cases
( q . i = TRUE or q . i = FALSE )
by XBOOLEAN:def 3;
suppose A34:
q . i = FALSE
;
z = (MergeSequence (p1,q1)) . jhence z =
X \ (p . i)
by A24, A25, Th3
.=
X \ (((id (rng p1)) * p) . i)
by A2, A5, A10, RELAT_1:53
.=
X \ (((p1 * (p1 ")) * p) . i)
by A21, FUNCT_1:39
.=
X \ ((p1 * ((p1 ") * p)) . i)
by RELAT_1:36
.=
X \ (p1 . j)
by A26, FUNCT_1:13
.=
(MergeSequence (p1,q1)) . j
by A31, A30, A34, Th3
;
verum end;
j in dom (MergeSequence (p1,q1))
by A28, Th1;
hence
z in rng (MergeSequence (p1,q1))
by A32, FUNCT_1:def 3;
verum
end;
then
{} = Intersect (rng (MergeSequence (p1,q1)))
by A12, SETFAM_1:44, XBOOLE_1:3;
hence
contradiction
by A3, A11, A19;
verum
end;
hence
Y is in_general_position
; verum