Mathlib Map

Theorems · Definition · general topology

IsometryEquiv.funUnique

(ι : Type u_2) → (α : Type u) → [inst : PseudoEMetricSpace α] → [Unique ι] → [inst_2 : Fintype ι] → (ι → α) ≃ᵢ α

Equiv.funUnique as an IsometryEquiv.

Defined in
Mathlib.Topology.MetricSpace.Isometry
Cited by
3 results in Mathlib
Foundations
Depth 151 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
PseudoEMetricSpaceUniqueFintype
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MeasureTheory.hausdorffMeasure_measurePreserving_funUnique · cited by 1MeasureTheory.hausdorffMe…IsometryEquiv.funUnique_symm_apply · cited by 0IsometryEquiv.funUnique_s…IsometryEquiv.funUnique_apply · cited by 0IsometryEquiv.funUnique_a…Equiv · cited by 8337EquivFintype · cited by 7736FintypePseudoEMetricSpace · cited by 1536PseudoEMetricSpaceUnique · cited by 400UniqueIsometryEquiv · cited by 177IsometryEquivEquiv.funUnique · cited by 22Equiv.funUniqueIsometryEquiv.funUniqueCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by3

Results whose statement or proof uses this declaration.