interior_union_left — Mathlib

English

If s is closed, then the interior of s ∪ t is contained in s ∪ interior(t).

Русский

Если s замкнуто, то interior(s ∪ t) ⊆ s ∪ interior(t).

LaTeX

$$$\\operatorname{int}(s \\cup t) \\subseteq s \\cup \\operatorname{int}(t)$$$

Lean4

theorem interior_union_left (_ : IsClosed s) : interior (s ∪ t) ⊆ s ∪ interior t := fun a ⟨u, ⟨⟨hu₁, hu₂⟩, ha⟩⟩ =>
  (Classical.em (a ∈ s)).imp_right fun h =>
    mem_interior.mpr
      ⟨u ∩ sᶜ, fun _x hx => (hu₂ hx.1).resolve_left hx.2, IsOpen.inter hu₁ IsClosed.isOpen_compl, ⟨ha, h⟩⟩

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