let T be TopSpace; for F being Subset-Family of T st F is finite holds
Int (meet F) = meet (Int F)
let F be Subset-Family of T; ( F is finite implies Int (meet F) = meet (Int F) )
assume A1:
F is finite
; Int (meet F) = meet (Int F)
A2:
meet (Int F) c= Int (meet F)
proof
consider p being
FinSequence such that A3:
rng p = F
by A1, FINSEQ_1:52;
consider n being
Nat such that A4:
dom p = Seg n
by FINSEQ_1:def 2;
defpred S1[
Nat]
means for
G being
Subset-Family of
T st
G = p .: (Seg $1) & $1
<= n & 1
<= n holds
meet (Int G) c= Int (meet G);
A5:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A6:
for
G being
Subset-Family of
T st
G = p .: (Seg k) &
k <= n & 1
<= n holds
meet (Int G) c= Int (meet G)
;
S1[k + 1]
let G be
Subset-Family of
T;
( G = p .: (Seg (k + 1)) & k + 1 <= n & 1 <= n implies meet (Int G) c= Int (meet G) )
assume A7:
G = p .: (Seg (k + 1))
;
( not k + 1 <= n or not 1 <= n or meet (Int G) c= Int (meet G) )
assume that A8:
k + 1
<= n
and A9:
1
<= n
;
meet (Int G) c= Int (meet G)
A10:
now ( 0 < k implies meet (Int G) c= Int (meet G) )reconsider G2 =
Im (
p,
(k + 1)) as
Subset-Family of
T by A3, RELAT_1:111, TOPS_2:2;
reconsider G1 =
p .: (Seg k) as
Subset-Family of
T by A3, RELAT_1:111, TOPS_2:2;
A11:
0 + 1
= 1
;
0 <= k
by NAT_1:2;
then
1
<= k + 1
by A11, XREAL_1:7;
then A12:
k + 1
in dom p
by A4, A8, FINSEQ_1:1;
then A13:
G2 = {(p . (k + 1))}
by FUNCT_1:59;
then
meet G2 = p . (k + 1)
by SETFAM_1:10;
then reconsider G3 =
p . (k + 1) as
Subset of
T ;
A14:
meet (Int G2) =
meet {(Int G3)}
by A13, Th19
.=
Int G3
by SETFAM_1:10
.=
Int (meet G2)
by A13, SETFAM_1:10
;
k + 1
<= n + 1
by A8, NAT_1:12;
then
k <= n
by XREAL_1:6;
then A15:
meet (Int G1) c= Int (meet G1)
by A6, A9;
assume
0 < k
;
meet (Int G) c= Int (meet G)then A16:
0 + 1
<= k
by NAT_1:13;
then A17:
k in Seg k
by FINSEQ_1:1;
k <= n
by A8, NAT_1:13;
then
k in dom p
by A4, A16, FINSEQ_1:1;
then A18:
p . k in G1
by A17, FUNCT_1:def 6;
k + 1
in {(k + 1)}
by TARSKI:def 1;
then A19:
p . (k + 1) in G2
by A12, FUNCT_1:def 6;
then A20:
Int G2 <> {}
by Th18;
A21:
p .: (Seg (k + 1)) =
p .: ((Seg k) \/ {(k + 1)})
by FINSEQ_1:9
.=
(p .: (Seg k)) \/ (p .: {(k + 1)})
by RELAT_1:120
;
then Int (meet G) =
Int ((meet G1) /\ (meet G2))
by A7, A18, A19, SETFAM_1:9
.=
(Int (meet G1)) /\ (Int (meet G2))
by TOPS_1:17
;
then A22:
(meet (Int G1)) /\ (meet (Int G2)) c= Int (meet G)
by A14, A15, XBOOLE_1:27;
Int G1 <> {}
by A18, Th18;
then
meet ((Int G1) \/ (Int G2)) c= Int (meet G)
by A20, A22, SETFAM_1:9;
hence
meet (Int G) c= Int (meet G)
by A7, A21, Th21;
verum end;
now ( k = 0 implies meet (Int G) c= Int (meet G) )assume A23:
k = 0
;
meet (Int G) c= Int (meet G)then
1
in dom p
by A4, A8, FINSEQ_1:1;
then A24:
Im (
p,1)
= {(p . 1)}
by FUNCT_1:59;
then
union G = p . 1
by A7, A23, FINSEQ_1:2, ZFMISC_1:25;
then reconsider G1 =
p . 1 as
Subset of
T ;
Int (meet G) =
Int G1
by A7, A23, A24, FINSEQ_1:2, SETFAM_1:10
.=
meet {(Int G1)}
by SETFAM_1:10
.=
meet (Int G)
by A7, A23, A24, Th19, FINSEQ_1:2
;
hence
meet (Int G) c= Int (meet G)
;
verum end;
hence
meet (Int G) c= Int (meet G)
by A10, NAT_1:3;
verum
end;
A25:
S1[
0 ]
by Th18, SETFAM_1:1;
A26:
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A25, A5);
hence
meet (Int F) c= Int (meet F)
by A27, A29;
verum
end;
Int (meet F) c= meet (Int F)
by Th28;
hence
Int (meet F) = meet (Int F)
by A2, XBOOLE_0:def 10; verum