Theorems · Definition · combinatorics

DiscreteTiling.Prototile.mk.noConfusion

{G : Type u_1} →
  {X : Type u_2} →
    {inst : Group G} →
      {inst_1 : MulAction G X} →
        {P : Sort u} →
          {carrier : Set X} →
            {symmetries : Subgroup ↥(MulAction.stabilizer G carrier)} →
              {carrier' : Set X} →
                {symmetries' : Subgroup ↥(MulAction.stabilizer G carrier')} →
                  { carrier := carrier, symmetries := symmetries } =
                      { carrier := carrier', symmetries := symmetries' } →
                    (carrier ≍ carrier' → symmetries ≍ symmetries' → P) → P

Defined in

Mathlib.Combinatorics.Tiling.Tile

Cited by

1 results in Mathlib

Foundations

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