Theorems · Definition · combinatorics

DiscreteTiling.Protoset.tiles

{G : Type u_1} →
  {X : Type u_2} →
    {ιₚ : Type u_3} →
      [inst : Group G] → [inst_1 : MulAction G X] → DiscreteTiling.Protoset G X ιₚ → ιₚ → DiscreteTiling.Prototile G X

The tiles in the protoset. Use the coercion to a function rather than using tiles directly.

Defined in

Mathlib.Combinatorics.Tiling.Tile

Cited by

22 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

GroupMulAction