closure_sInter_eq_biInter_closure_of_sUnion_indep

English

Same as above for sInter with a nonempty index set.

Русский

То же самое для sInter по непустому индексу.

LaTeX

$$$\operatorname{Indep}(I) \rightarrow \operatorname{cl}(\bigcap J_i) = \bigcap \operatorname{cl}(J_i)$$$

Lean4

theorem closure_sInter_eq_biInter_closure_of_sUnion_indep (Is : Set (Set α)) (hIs : Is.Nonempty) (h : M.Indep (⋃₀ Is)) :
    M.closure (⋂₀ Is) = (⋂ I ∈ Is, M.closure I) :=
  h.closure_sInter_eq_biInter_closure_of_forall_subset hIs (fun _ ↦ subset_sUnion_of_mem)

Похожие утверждения