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