Theorems · Theorem · convex and discrete geometry

Delone.DeloneSet.mapBilipschitz.congr_simp

∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (f f_1 : X ≃ Y) (e_f : f = f_1)
  (K₁ K₁_1 : NNReal) (e_K₁ : K₁ = K₁_1) (K₂ K₂_1 : NNReal) (e_K₂ : K₂ = K₂_1) (hK₁ : 0 < K₁) (hK₂ : 0 < K₂)
  (hf₁ : AntilipschitzWith K₁ ⇑f) (hf₂ : LipschitzWith K₂ ⇑f) (D D_1 : Delone.DeloneSet X),
  D = D_1 →
    Delone.DeloneSet.mapBilipschitz f K₁ K₂ hK₁ hK₂ hf₁ hf₂ D =
      Delone.DeloneSet.mapBilipschitz f_1 K₁_1 K₂_1 ⋯ ⋯ ⋯ ⋯ D_1

Defined in

Mathlib.Analysis.AperiodicOrder.Delone.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

MetricSpaceMetricSpace