let T be TopSpace; :: thesis: 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; :: thesis: ( F is finite implies Int (meet F) = meet (Int F) )
assume A1:
F is finite
; :: thesis: 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:73;
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:
S1[
0 ]
A7:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A8:
for
G being
Subset-Family of
T st
G = p .: (Seg k) &
k <= n & 1
<= n holds
meet (Int G) c= Int (meet G)
;
:: thesis: S1[k + 1]
let G be
Subset-Family of
T;
:: thesis: ( G = p .: (Seg (k + 1)) & k + 1 <= n & 1 <= n implies meet (Int G) c= Int (meet G) )
assume A9:
G = p .: (Seg (k + 1))
;
:: thesis: ( not k + 1 <= n or not 1 <= n or meet (Int G) c= Int (meet G) )
assume A10:
(
k + 1
<= n & 1
<= n )
;
:: thesis: meet (Int G) c= Int (meet G)
A11:
now assume A12:
k = 0
;
:: thesis: meet (Int G) c= Int (meet G)then
(
Seg (k + 1) = {1} & 1
in dom p )
by A4, A10, FINSEQ_1:3, FINSEQ_1:4;
then A13:
Im p,1
= {(p . 1)}
by FUNCT_1:117;
then
union G = p . 1
by A9, A12, FINSEQ_1:4, ZFMISC_1:31;
then reconsider G1 =
p . 1 as
Subset of
T ;
Int (meet G) =
Int G1
by A9, A12, A13, FINSEQ_1:4, SETFAM_1:11
.=
meet {(Int G1)}
by SETFAM_1:11
.=
meet (Int G)
by A9, A12, A13, Th20, FINSEQ_1:4
;
hence
meet (Int G) c= Int (meet G)
;
:: thesis: verum end;
now assume A14:
0 < k
;
:: thesis: meet (Int G) c= Int (meet G)A15:
p .: (Seg (k + 1)) =
p .: ((Seg k) \/ {(k + 1)})
by FINSEQ_1:11
.=
(p .: (Seg k)) \/ (p .: {(k + 1)})
by RELAT_1:153
;
reconsider G1 =
p .: (Seg k) as
Subset-Family of
T by A3, RELAT_1:144, TOPS_2:3;
reconsider G2 =
Im p,
(k + 1) as
Subset-Family of
T by A3, RELAT_1:144, TOPS_2:3;
(
0 <= k &
0 + 1
= 1 )
by NAT_1:2;
then
( 1
<= k + 1 &
k + 1
<= n )
by A10, XREAL_1:9;
then A16:
k + 1
in dom p
by A4, FINSEQ_1:3;
(
0 + 1
<= k &
k <= k + 1 )
by A14, NAT_1:13;
then
( 1
<= k &
k <= n )
by A10, XXREAL_0:2;
then
(
k in Seg k &
k + 1
in {(k + 1)} &
k in dom p )
by A4, FINSEQ_1:3, TARSKI:def 1;
then A17:
(
p . k in G1 &
p . (k + 1) in G2 )
by A16, FUNCT_1:def 12;
then A18:
(
Int G1 <> {} &
Int G2 <> {} )
by Th19;
A19:
Int (meet G) =
Int ((meet G1) /\ (meet G2))
by A9, A15, A17, SETFAM_1:10
.=
(Int (meet G1)) /\ (Int (meet G2))
by TOPS_1:46
;
A20:
G2 = {(p . (k + 1))}
by A16, FUNCT_1:117;
then
(
meet G2 = p . (k + 1) &
p . (k + 1) in F )
by A3, A16, FUNCT_1:def 5, SETFAM_1:11;
then reconsider G3 =
p . (k + 1) as
Subset of
T ;
A21:
meet (Int G2) =
meet {(Int G3)}
by A20, Th20
.=
Int G3
by SETFAM_1:11
.=
Int (meet G2)
by A20, SETFAM_1:11
;
k + 1
<= n + 1
by A10, NAT_1:12;
then
k <= n
by XREAL_1:8;
then
meet (Int G1) c= Int (meet G1)
by A8, A10;
then
(meet (Int G1)) /\ (meet (Int G2)) c= Int (meet G)
by A19, A21, XBOOLE_1:27;
then
meet ((Int G1) \/ (Int G2)) c= Int (meet G)
by A18, SETFAM_1:10;
hence
meet (Int G) c= Int (meet G)
by A9, A15, Th22;
:: thesis: verum end;
hence
meet (Int G) c= Int (meet G)
by A11, NAT_1:3;
:: thesis: verum
end;
A22:
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A5, A7);
hence
meet (Int F) c= Int (meet F)
by A23, A24;
:: thesis: verum
end;
Int (meet F) c= meet (Int F)
by Th29;
hence
Int (meet F) = meet (Int F)
by A2, XBOOLE_0:def 10; :: thesis: verum