dist_pi_lt_iff — Mathlib

English

Let f,g: β → X_b and hr: r>0. Then dist(f,g) < r iff for all b, dist(f(b),g(b)) < r.

Русский

Для функций f,g: β → X_b и hr: r>0 верно: dist(f,g) < r тогда и только тогда, когда для каждого b выполняется dist(f(b),g(b)) < r.

LaTeX

$$$\mathrm{dist}(f,g) < r \iff \forall b \in \mathrm{univ}, \mathrm{dist}(f(b),g(b)) < r.$$$

Lean4

theorem dist_pi_lt_iff {f g : ∀ b, X b} {r : ℝ} (hr : 0 < r) : dist f g < r ↔ ∀ b, dist (f b) (g b) < r :=
  by
  lift r to ℝ≥0 using hr.le
  exact nndist_pi_lt_iff hr

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