English
If s is closed and interior(t) is empty, then interior(s ∪ t) = interior(s).
Русский
Если s замкнуто и interior(t) = ∅, то interior(s ∪ t) = interior(s).
LaTeX
$$$ IsClosed(s) \wedge \operatorname{int}(t) = \emptyset \Rightarrow \operatorname{int}(s \cup t) = \operatorname{int}(s)$$$
Lean4
theorem interior_union_isClosed_of_interior_empty (h₁ : IsClosed s) (h₂ : interior t = ∅) :
interior (s ∪ t) = interior s :=
have : interior (s ∪ t) ⊆ s := fun x ⟨u, ⟨(hu₁ : IsOpen u), (hu₂ : u ⊆ s ∪ t)⟩, (hx₁ : x ∈ u)⟩ =>
by_contradiction fun hx₂ : x ∉ s =>
have : u \ s ⊆ t := fun _ ⟨h₁, h₂⟩ => Or.resolve_left (hu₂ h₁) h₂
have : u \ s ⊆ interior t := by rwa [(IsOpen.sdiff hu₁ h₁).subset_interior_iff]
have : u \ s ⊆ ∅ := by rwa [h₂] at this
this ⟨hx₁, hx₂⟩
Subset.antisymm (interior_maximal this isOpen_interior) (interior_mono subset_union_left)
