Theorems · Definition · combinatorics

DiscreteTiling.PlacedTile.casesOn

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

Defined in

Mathlib.Combinatorics.Tiling.Tile

Cited by

5 results in Mathlib

Foundations

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

Assumes

GroupMulAction