dist_pi_le_iff — Mathlib

English

For f,g: β → X_b and any r, dist(f,g) ≤ r iff for all b, dist(f(b),g(b)) ≤ r.

Русский

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

LaTeX

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

Lean4

theorem dist_pi_le_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
  exact nndist_pi_le_iff

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