some — Mathlib

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⟩

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