nndist_pi_le_iff — Mathlib

English

For f,g: β → X_b, the inequality nndist(f,g) ≤ r is equivalent to nndist(f(b),g(b)) ≤ r for every b ∈ β.

Русский

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

LaTeX

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

Lean4

theorem nndist_pi_le_iff {f g : ∀ b, X b} {r : ℝ≥0} : nndist f g ≤ r ↔ ∀ b, nndist (f b) (g b) ≤ r := by
  simp [nndist_pi_def]

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