A set union the interior of its complement is dense

Stream: Is there code for X?

[Felix Weilacher]

Do we have anything similar to the following?

variable {α : Type*} [TopologicalSpace α]

theorem union_interior_compl_dense {s : Set α} :
    Dense (s ∪ interior sᶜ) := by
  rw [dense_iff_closure_eq, closure_union, ←univ_subset_iff]
  refine' subset_trans _ (union_subset_union_right _ (subset_closure))
  simp

[Yury G. Kudryashov]

Loogle finds nothing. BTW, another version to formulate this lemma is Dense (closure s \ s)ᶜ

[Felix Weilacher]

That's probably a better spelling