single — Mathlib

English

Any Pi.single construction yields an isometry.

Русский

Построение Pi.single является изометрией.

LaTeX

$$$Isometry\\ (Pi.single(i))$$$

Lean4

protected theorem single [Fintype ι] [DecidableEq ι] {E : ι → Type*} [∀ i, PseudoEMetricSpace (E i)] [∀ i, Zero (E i)]
    (i : ι) : Isometry (Pi.single (M := E) i) := by
  intro x y
  rw [edist_pi_def]
  refine le_antisymm (Finset.sup_le fun j ↦ ?_) (Finset.le_sup_of_le (Finset.mem_univ i) (by simp))
  obtain rfl | h := eq_or_ne i j
  · simp
  · simp [h]

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