English
Given a function f with dense range, and an open nonempty set s, there exists an a with f(a) ∈ s.
Русский
Пусть функция f имеет плотный образ, и задано открытое непустое множество s; тогда существует a с f(a) ∈ s.
LaTeX
$$(hf : \mathrm{DenseRange} f) (ho : IsOpen s) (hs : s.Nonempty) : ∃ a, f a ∈ s$$
Lean4
/-- Given a function `f : X → Y` with dense range and `y : Y`, returns some `x : X`. -/
noncomputable def some (hf : DenseRange f) (x : X) : α :=
Classical.choice <| hf.nonempty_iff.mpr ⟨x⟩