Theorems · Theorem · convex and discrete geometry

Delone.DeloneSet.mapIsometry_trans

∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {Z : Type u_3} [inst_2 : MetricSpace Z]
  (D : Delone.DeloneSet X) (f : X ≃ᵢ Y) (g : Y ≃ᵢ Z),
  (Delone.DeloneSet.mapIsometry (f.trans g)) D = (Delone.DeloneSet.mapIsometry g) ((Delone.DeloneSet.mapIsometry f) D)

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

MetricSpaceMetricSpaceMetricSpace