nndist_pi_lt_iff — Mathlib

English

For f,g: β → X_b and positive r, nndist(f,g) < r if and only if for all b, nndist(f(b),g(b)) < r.

Русский

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

LaTeX

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

Lean4

theorem nndist_pi_lt_iff {f g : ∀ b, X b} {r : ℝ≥0} (hr : 0 < r) : nndist f g < r ↔ ∀ b, nndist (f b) (g b) < r := by
  simp [nndist_pi_def, Finset.sup_lt_iff hr]

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