Theorems · Theorem · general topology

Fin.appendIsometry_apply

∀ {α : Type u} [inst : PseudoEMetricSpace α] (m n : ℕ) (fg : (Fin m → α) × (Fin n → α)) (a : Fin (m + n)),
  (Fin.appendIsometry m n) fg a = Fin.append fg.1 fg.2 a

Defined in

Mathlib.Topology.MetricSpace.Isometry

Cited by

0 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpace