closure_iInter_eq_iInter_closure_of_iUnion_indep

English

If I is independent, then closure of an iInter equals the iInter of closures over a family.

Русский

Если I независим, тогда cl(⋂ i Js) = ⋂ i cl(Js).

LaTeX

$$$\operatorname{Indep}(I) \rightarrow \operatorname{cl}\left(\bigcap_{i} J_i\right) = \bigcap_{i} \operatorname{cl}(J_i)$$$

Lean4

theorem closure_iInter_eq_iInter_closure_of_iUnion_indep [hι : Nonempty ι] (Is : ι → Set α) (h : M.Indep (⋃ i, Is i)) :
    M.closure (⋂ i, Is i) = (⋂ i, M.closure (Is i)) :=
  by
  convert h.closure_sInter_eq_biInter_closure_of_forall_subset (range_nonempty Is) (by simp [subset_iUnion])
  simp

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