Theorems · Theorem · combinatorics

DiscreteTiling.Prototile.mk.inj

∀ {G : Type u_1} {X : Type u_2} {inst : Group G} {inst_1 : MulAction G X} {carrier : Set X}
  {symmetries : Subgroup ↥(MulAction.stabilizer G carrier)} {carrier_1 : Set X}
  {symmetries_1 : Subgroup ↥(MulAction.stabilizer G carrier_1)},
  { carrier := carrier, symmetries := symmetries } = { carrier := carrier_1, symmetries := symmetries_1 } →
    carrier = carrier_1 ∧ symmetries ≍ symmetries_1

Defined in

Mathlib.Combinatorics.Tiling.Tile

Cited by

1 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound