Theorems · Definition · combinatorics

DiscreteTiling.PlacedTile.mk.noConfusion

{G : Type u_1} →
  {X : Type u_2} →
    {ιₚ : Type u_3} →
      {inst : Group G} →
        {inst_1 : MulAction G X} →
          {ps : DiscreteTiling.Protoset G X ιₚ} →
            {P : Sort u} →
              {index : ιₚ} →
                {groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries} →
                  {index' : ιₚ} →
                    {groupElts' :
                        G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index')).subtype (↑ps index').symmetries} →
                      { index := index, groupElts := groupElts } = { index := index', groupElts := groupElts' } →
                        (index ≍ index' → groupElts ≍ groupElts' → P) → P

Defined in

Mathlib.Combinatorics.Tiling.Tile

Cited by

1 results in Mathlib

Foundations

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