Theorems · Theorem · general topology

Fin.appendIsometry_symm_apply

∀ {α : Type u} [inst : PseudoEMetricSpace α] (m n : ℕ) (f : Fin (m + n) → α),
  (Fin.appendIsometry m n).symm f = (fun i => f (Fin.castAdd n i), fun i => f (Fin.natAdd m i))

Defined in

Mathlib.Topology.MetricSpace.Isometry

Cited by

0 results in Mathlib

Foundations

Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpace