mem_closure_range_iff — Mathlib

English

An element lies in the closure of the range of a map e:β→α iff every ε>0 is achieved by some e(k) within ε of a.

Русский

Точка принадлежит замыканию образа e:β→α тогда и только тогда, когда для каждого ε>0 существует k так, что dist(a,e(k))<ε.

LaTeX

$$$a \in \overline{\operatorname{range}(e)} \iff \forall \varepsilon>0, \exists k, \operatorname{dist}(a, e(k)) < \varepsilon$$$

Lean4

theorem mem_closure_range_iff {e : β → α} {a : α} : a ∈ closure (range e) ↔ ∀ ε > 0, ∃ k : β, dist a (e k) < ε := by
  simp only [mem_closure_iff, exists_range_iff]

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