closure_inter_of_codisjoint_interior

English

If interior s and interior t are codisjoint, then closure(s ∩ t) = closure s ∩ closure t.

Русский

Если interior s и interior t кодизпособны, то cl(s ∩ t) = cl(s) ∩ cl(t).

LaTeX

$$$\\\\text{Codisjoint}(\\\\operatorname{int}(s), \\\\operatorname{int}(t)) \\\\Rightarrow \\\\overline{s \\cap t} = \\\\overline{s} \\cap \\\\overline{t}$$$

Lean4

theorem closure_inter_of_codisjoint_interior (h : Codisjoint (interior s) (interior t)) :
    closure (s ∩ t) = closure s ∩ closure t := by
  rw [← compl_inj_iff]
  simp only [← interior_compl, compl_inter]
  apply interior_union_of_disjoint_closure
  simpa only [closure_compl, disjoint_compl_left_iff, ← codisjoint_iff_compl_le_left]

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