mem_closure_range_iff_nat — Mathlib

English

An element lies in the closure of the range iff it can be approximated by the sequence e(k) with bounds 1/(n+1).

Русский

Элемент принадлежит замыканию образа, если он может аппроксимироваться последовательностью e(k) с ограничениями 1/(n+1).

LaTeX

$$$a \in \overline{\operatorname{range}(e)} \iff \forall n \in \mathbb{N}, \exists k, \operatorname{dist}(a, e(k)) < \frac{1}{n+1}$$$

Lean4

theorem mem_closure_range_iff_nat {e : β → α} {a : α} :
    a ∈ closure (range e) ↔ ∀ n : ℕ, ∃ k : β, dist a (e k) < 1 / ((n : ℝ) + 1) :=
  (mem_closure_iff_nhds_basis nhds_basis_ball_inv_nat_succ).trans <| by
    simp only [mem_ball, dist_comm, exists_range_iff, forall_const]

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