English
In a Fin- indexed product, the distance between two insertNth-assembled elements equals the maximum of the distance of the inserted elements and the distance of the remaining parts.
Русский
В произведении с индексами Fin расстояние между двумя элементами, полученными вставками, равно максимуму между расстоянием вставляемых элементов и расстоянием оставшихся частей.
LaTeX
$$$\mathrm{nndist}(i\!\operatorname{insertNth} x f, i\!\operatorname{insertNth} y g) = \max( \mathrm{nndist}(x,y), \mathrm{nndist}(f,g) ).$$$
Lean4
@[simp]
theorem nndist_insertNth_insertNth {n : ℕ} {α : Fin (n + 1) → Type*} [∀ i, PseudoMetricSpace (α i)] (i : Fin (n + 1))
(x y : α i) (f g : ∀ j, α (i.succAbove j)) :
nndist (i.insertNth x f) (i.insertNth y g) = max (nndist x y) (nndist f g) :=
eq_of_forall_ge_iff fun c => by simp [nndist_pi_le_iff, i.forall_iff_succAbove]
