exists_mem_open — Mathlib

English

If s is dense in X, and U is open with U nonempty, then there exists x in s ∩ U.

Русский

Если s плотно в X, и U открыто и непусто, существует точка x, принадлежащая s и лежащая в U.

LaTeX

$$$\operatorname{Dense}(s) \rightarrow \mathrm{IsOpen}(U) \rightarrow U \neq \emptyset \rightarrow \exists x (x \in s \land x \in U)$$$

Lean4

theorem exists_mem_open (hs : Dense s) {U : Set X} (ho : IsOpen U) (hne : U.Nonempty) : ∃ x ∈ s, x ∈ U :=
  let ⟨x, hx⟩ := hs.inter_open_nonempty U ho hne
  ⟨x, hx.2, hx.1⟩

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