dist_pi_eq_iff — Mathlib

English

For f,g: β → X_b and r>0, dist(f,g) = r iff there exists i with dist(f(i),g(i)) = r and for all b, dist(f(b),g(b)) ≤ r.

Русский

Пусть f,g: β → X_b и r>0. Тогда dist(f,g)=r тогда же, когда существует i с dist(f(i),g(i))=r и для всех b выполняется dist(f(b),g(b)) ≤ r.

LaTeX

$$$\mathrm{dist}(f,g) = r \iff \big(\exists i, \mathrm{dist}(f(i),g(i)) = r\big) \land \forall b \in \mathrm{univ}, \mathrm{dist}(f(b),g(b)) \le r.$$$

Lean4

theorem dist_pi_eq_iff {f g : ∀ b, X b} {r : ℝ} (hr : 0 < r) :
    dist f g = r ↔ (∃ i, dist (f i) (g i) = r) ∧ ∀ b, dist (f b) (g b) ≤ r :=
  by
  lift r to ℝ≥0 using hr.le
  simp_rw [← coe_nndist, NNReal.coe_inj, nndist_pi_eq_iff hr, NNReal.coe_le_coe]

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