mem_nhds — Mathlib

English

For every x and every neighborhood s of x, there exists a ∈ domain with f(a) ∈ s.

Русский

Для каждого x и каждой окрестности s(x) существует a такое, что f(a) ∈ s.

LaTeX

$$(h : \mathrm{DenseRange} f) (hs : s ∈ 𝓝 x) : ∃ a, f a ∈ s$$

Lean4

theorem mem_nhds (h : DenseRange f) (hs : s ∈ 𝓝 x) : ∃ a, f a ∈ s :=
  let ⟨a, ha⟩ := h.exists_mem_open isOpen_interior ⟨x, mem_interior_iff_mem_nhds.2 hs⟩
  ⟨a, interior_subset ha⟩

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