English
For f,g: β → X_b and r>0, nndist(f,g) = r holds if and only if there exists i with nndist(f(i),g(i)) = r and for all b, nndist(f(b),g(b)) ≤ r.
Русский
Пусть f,g: β → X_b и r>0. Тогда nndist(f,g)=r тогда же, когда существует i с nndist(f(i),g(i))=r и для всех b выполняется nndist(f(b),g(b)) ≤ r.
LaTeX
$$$\mathrm{nndist}(f,g) = r \iff \big(\exists i, \mathrm{nndist}(f(i),g(i)) = r\big) \land \forall b \in \mathrm{univ}, \mathrm{nndist}(f(b),g(b)) \le r.$$$
Lean4
theorem nndist_pi_eq_iff {f g : ∀ b, X b} {r : ℝ≥0} (hr : 0 < r) :
nndist f g = r ↔ (∃ i, nndist (f i) (g i) = r) ∧ ∀ b, nndist (f b) (g b) ≤ r :=
by
rw [eq_iff_le_not_lt, nndist_pi_lt_iff hr, nndist_pi_le_iff, not_forall, and_comm]
simp_rw [not_lt, and_congr_left_iff, le_antisymm_iff]
intro h
refine exists_congr fun b => ?_
apply (and_iff_right <| h _).symm
