Theorems · Definition · combinatorics

DiscreteTiling.Prototile.carrier

{G : Type u_1} → {X : Type u_2} → [inst : Group G] → [inst_1 : MulAction G X] → DiscreteTiling.Prototile G X → Set X

The points in the prototile. Use the coercion to Set X, or ∈ on the Prototile, rather than using carrier directly. The coercion cannot use SetLike because it does not satisfy coe_injective.

Defined in

Mathlib.Combinatorics.Tiling.Tile

Cited by

21 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

GroupMulAction