closure_iInter_eq_biInter_closure_of_forall_subset

English

See above for a variant with biUnion of index set.

Русский

См. выше для варианта с би-объединением индексов.

LaTeX

$$$A \neq \varnothing \Rightarrow \operatorname{cl}\left(\bigcap_{i \in A} I_i\right) = \bigcap_{i \in A} \operatorname{cl}(I_i)$$$

Lean4

theorem closure_iInter_eq_biInter_closure_of_forall_subset [Nonempty ι] {Js : ι → Set α} (hI : M.Indep I)
    (hJs : ∀ i, Js i ⊆ I) : M.closure (⋂ i, Js i) = ⋂ i, M.closure (Js i) :=
  closure_iInter_eq_iInter_closure_of_iUnion_indep _ (hI.subset <| by simpa)

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