Mathlib Map

Theorems · Theorem · convex and discrete geometry

Delone.DeloneSet.mapIsometry_symm

∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (f : X ≃ᵢ Y),
  (Delone.DeloneSet.mapIsometry f).symm = Delone.DeloneSet.mapIsometry f.symm
Defined in
Mathlib.Analysis.AperiodicOrder.Delone.Basic
Cited by
0 results in Mathlib
Foundations
Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
MetricSpaceMetricSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Equiv · cited by 8337EquivEquiv.symm · cited by 3681Equiv.symmMetricSpace · cited by 1684MetricSpaceIsometryEquiv · cited by 177IsometryEquivIsometryEquiv.symm · cited by 75IsometryEquiv.symmDelone.DeloneSet · cited by 34Delone.DeloneSetDelone.DeloneSet.mapIsometry · cited by 9DeloneSet.mapIsometryDeloneSet.mapIsometry_symmCITED BYCITES

Cites7

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

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.