closure_inter_eq_inter_closure — Mathlib

English

If I ∪ J is independent, then cl(I ∩ J) = cl(I) ∩ cl(J).

Русский

Если I ∪ J независим, то cl(I ∩ J) = cl(I) ∩ cl(J).

LaTeX

$$$\operatorname{Indep}(I \cup J) \Rightarrow \operatorname{cl}(I \cap J) = \operatorname{cl}(I) \cap \operatorname{cl}(J)$$$

Lean4

theorem closure_inter_eq_inter_closure (h : M.Indep (I ∪ J)) : M.closure (I ∩ J) = M.closure I ∩ M.closure J :=
  by
  rw [inter_eq_iInter, closure_iInter_eq_iInter_closure_of_iUnion_indep, inter_eq_iInter]
  · exact iInter_congr (by simp)
  rwa [← union_eq_iUnion]

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