Theorems · Theorem · combinatorics

DiscreteTiling.Prototile.mk.injEq

∀ {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

0 results in Mathlib

Foundations

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

Assumes

GroupMulAction