subset_closure_inter_of_isPreirreducible_of_isOpen

English

If S is preirreducible and U is open and nonempty contained in S, then S is contained in the closure of S ∩ U.

Русский

Если S преднеразложимо, и U открыто, непусто и содержится в S, тогда S содержится в замыкании S ∩ U.

LaTeX

$$$\mathrm{IsPreirreducible}(S) \rightarrow \mathrm{IsOpen}(U) \rightarrow (S \cap U).\mathrm{Nonempty} \rightarrow S \subseteq \overline{S \cap U}$$$

Lean4

/-- A nonempty open subset of a preirreducible subspace is dense in the subspace. -/
theorem subset_closure_inter_of_isPreirreducible_of_isOpen {S U : Set X} (hS : IsPreirreducible S) (hU : IsOpen U)
    (h : (S ∩ U).Nonempty) : S ⊆ closure (S ∩ U) := by
  by_contra h'
  obtain ⟨x, h₁, h₂, h₃⟩ := hS _ (closure (S ∩ U))ᶜ hU isClosed_closure.isOpen_compl h (inter_compl_nonempty_iff.mpr h')
  exact h₃ (subset_closure ⟨h₁, h₂⟩)

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