Theorems · Theorem · general topology

Fin.appendHomeomorph_symm_apply

∀ {X : Type u_1} [inst : TopologicalSpace X] (m n : ℕ) (f : Fin (m + n) → X),
  (Fin.appendHomeomorph m n).symm f = (fun i => f (Fin.castAdd n i), fun i => f (Fin.natAdd m i))

Defined in

Mathlib.Topology.Homeomorph.Lemmas

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace