Theorems · Inductive type · combinatorics

DiscreteTiling.Protoset

(G : Type u_1) → (X : Type u_2) → Type u_3 → [inst : Group G] → [MulAction G X] → Type (max (max u_1 u_2) u_3)

A Protoset G X ιₚ is an indexed family of Prototile G X. This is a separate definition rather than just using plain functions to facilitate defining associated API that can be used with dot notation.

Defined in

Mathlib.Combinatorics.Tiling.Tile

Cited by

29 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

GroupMulAction