Tile

📁 Source: Mathlib/Combinatorics/Tiling/Tile.lean

Statistics

Metric	Count
Definitions PlacedTile, coeSet, groupElts, index, instCoeOutSet, instMembership, instMulAction, instSMul, Protoset, instCoeFunForallPrototile, instInhabited, tiles, Prototile, carrier, instCoeOutSet, instInhabited, instMembership, symmetries	18
Theorems coe_finite_iff, coe_mk_coe, coe_mk_finite_iff, coe_mk_mk, coe_mk_nonempty_iff, coe_nonempty_iff, coe_smul, ext, ext_iff, ext_iff_of_exists, ext_iff_of_preimage, induction_on, instNonempty, mem_coe, mem_inv_smul_iff_smul_mem, mem_smul_iff_smul_inv_mem, smul_index, smul_mem_smul_iff, smul_mk_coe, smul_mk_mk, coe_inj, coe_injective, coe_mk, ext, ext_iff, coe_mk, ext, ext_iff, mem_coe	29
Total	47

DiscreteTiling

Definitions

Name	Category	Theorems
PlacedTile 📖	CompData	9 math math: PlacedTile.smul_mk_mk, PlacedTile.mem_inv_smul_iff_smul_mem, PlacedTile.smul_index, PlacedTile.mem_coe, PlacedTile.mem_smul_iff_smul_inv_mem, PlacedTile.instNonempty, PlacedTile.smul_mk_coe, PlacedTile.coe_smul, PlacedTile.smul_mem_smul_iff
Protoset 📖	CompData	1 math math: Protoset.coe_injective
Prototile 📖	CompData	1 math math: Prototile.mem_coe

DiscreteTiling.PlacedTile

Definitions

Name	Category	Theorems
coeSet 📖	CompOp	8 math math: coe_finite_iff, coe_mk_finite_iff, coe_nonempty_iff, mem_coe, coe_mk_mk, coe_smul, coe_mk_nonempty_iff, coe_mk_coe
groupElts 📖	CompOp	3 math math: ext_iff_of_preimage, ext_iff_of_exists, ext_iff
index 📖	CompOp	6 math math: ext_iff_of_preimage, ext_iff_of_exists, ext_iff, coe_finite_iff, smul_index, coe_nonempty_iff
instCoeOutSet 📖	CompOp	—
instMembership 📖	CompOp	4 math math: mem_inv_smul_iff_smul_mem, mem_coe, mem_smul_iff_smul_inv_mem, smul_mem_smul_iff
instMulAction 📖	CompOp	—
instSMul 📖	CompOp	7 math math: smul_mk_mk, mem_inv_smul_iff_smul_mem, smul_index, mem_smul_iff_smul_inv_mem, smul_mk_coe, coe_smul, smul_mem_smul_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_finite_iff 📖	mathematical	—	Set.Finite coeSet DiscreteTiling.Prototile.carrier DiscreteTiling.Protoset.tiles index	—	Quotient.out_eq' Quotient.liftOn'_mk''
coe_mk_coe 📖	mathematical	—	coeSet Subgroup.map Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid DiscreteTiling.Prototile.carrier DiscreteTiling.Protoset.tiles Subgroup.toGroup Subgroup.subtype DiscreteTiling.Prototile.symmetries Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	—
coe_mk_finite_iff 📖	mathematical	—	Set.Finite coeSet DiscreteTiling.Prototile.carrier DiscreteTiling.Protoset.tiles	—	coe_finite_iff
coe_mk_mk 📖	mathematical	—	coeSet QuotientGroup.leftRel Subgroup.map Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid DiscreteTiling.Prototile.carrier DiscreteTiling.Protoset.tiles Subgroup.toGroup Subgroup.subtype DiscreteTiling.Prototile.symmetries Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	—
coe_mk_nonempty_iff 📖	mathematical	—	Set.Nonempty coeSet DiscreteTiling.Prototile.carrier DiscreteTiling.Protoset.tiles	—	coe_nonempty_iff
coe_nonempty_iff 📖	mathematical	—	Set.Nonempty coeSet DiscreteTiling.Prototile.carrier DiscreteTiling.Protoset.tiles index	—	Quotient.out_eq' Quotient.liftOn'_mk''
coe_smul 📖	mathematical	—	coeSet DiscreteTiling.PlacedTile instSMul Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	induction_on SemigroupAction.mul_smul
ext 📖	—	index HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup Subgroup.map SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid DiscreteTiling.Prototile.carrier DiscreteTiling.Protoset.tiles Subgroup.toGroup Subgroup.subtype DiscreteTiling.Prototile.symmetries groupElts	—	—	—
ext_iff 📖	mathematical	—	index HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup Subgroup.map SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid DiscreteTiling.Prototile.carrier DiscreteTiling.Protoset.tiles Subgroup.toGroup Subgroup.subtype DiscreteTiling.Prototile.symmetries groupElts	—	ext
ext_iff_of_exists 📖	mathematical	—	index QuotientGroup.leftRel Subgroup.map Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid DiscreteTiling.Prototile.carrier DiscreteTiling.Protoset.tiles Subgroup.toGroup Subgroup.subtype DiscreteTiling.Prototile.symmetries groupElts	—	Quotient.out_eq ext
ext_iff_of_preimage 📖	mathematical	—	index Set.preimage QuotientGroup.leftRel Subgroup.map Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid DiscreteTiling.Prototile.carrier DiscreteTiling.Protoset.tiles Subgroup.toGroup Subgroup.subtype DiscreteTiling.Prototile.symmetries HasQuotient.Quotient QuotientGroup.instHasQuotientSubgroup Set.instSingletonSet groupElts	—	ext Set.singleton_eq_singleton_iff Set.preimage_eq_preimage Quotient.mk''_surjective
induction_on 📖	—	Subgroup.map Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid DiscreteTiling.Prototile.carrier DiscreteTiling.Protoset.tiles Subgroup.toGroup Subgroup.subtype DiscreteTiling.Prototile.symmetries	—	—	Quotient.inductionOn'
instNonempty 📖	mathematical	—	DiscreteTiling.PlacedTile	—	—
mem_coe 📖	mathematical	—	Set Set.instMembership coeSet DiscreteTiling.PlacedTile instMembership	—	—
mem_inv_smul_iff_smul_mem 📖	mathematical	—	DiscreteTiling.PlacedTile instMembership instSMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	coe_smul
mem_smul_iff_smul_inv_mem 📖	mathematical	—	DiscreteTiling.PlacedTile instMembership instSMul SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	coe_smul
smul_index 📖	mathematical	—	index DiscreteTiling.PlacedTile instSMul	—	induction_on
smul_mem_smul_iff 📖	mathematical	—	DiscreteTiling.PlacedTile instMembership instSMul SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	mem_coe coe_smul Set.smul_mem_smul_set_iff
smul_mk_coe 📖	mathematical	—	DiscreteTiling.PlacedTile instSMul Subgroup.map Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid DiscreteTiling.Prototile.carrier DiscreteTiling.Protoset.tiles Subgroup.toGroup Subgroup.subtype DiscreteTiling.Prototile.symmetries MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
smul_mk_mk 📖	mathematical	—	DiscreteTiling.PlacedTile instSMul QuotientGroup.leftRel Subgroup.map Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid DiscreteTiling.Prototile.carrier DiscreteTiling.Protoset.tiles Subgroup.toGroup Subgroup.subtype DiscreteTiling.Prototile.symmetries MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—

DiscreteTiling.Protoset

Definitions

Name	Category	Theorems
instCoeFunForallPrototile 📖	CompOp	—
instInhabited 📖	CompOp	—
tiles 📖	CompOp	15 math math: coe_mk, DiscreteTiling.PlacedTile.ext_iff_of_preimage, DiscreteTiling.PlacedTile.ext_iff_of_exists, DiscreteTiling.PlacedTile.smul_mk_mk, DiscreteTiling.PlacedTile.ext_iff, DiscreteTiling.PlacedTile.coe_finite_iff, DiscreteTiling.PlacedTile.coe_mk_finite_iff, DiscreteTiling.PlacedTile.coe_nonempty_iff, DiscreteTiling.PlacedTile.coe_mk_mk, DiscreteTiling.PlacedTile.smul_mk_coe, coe_inj, coe_injective, ext_iff, DiscreteTiling.PlacedTile.coe_mk_nonempty_iff, DiscreteTiling.PlacedTile.coe_mk_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_inj 📖	mathematical	—	tiles	—	ext_iff
coe_injective 📖	mathematical	—	DiscreteTiling.Protoset tiles	—	—
coe_mk 📖	mathematical	—	tiles	—	—
ext 📖	—	tiles	—	—	—
ext_iff 📖	mathematical	—	tiles	—	ext

DiscreteTiling.Prototile

Definitions

Name	Category	Theorems
carrier 📖	CompOp	14 math math: mem_coe, DiscreteTiling.PlacedTile.ext_iff_of_preimage, DiscreteTiling.PlacedTile.ext_iff_of_exists, DiscreteTiling.PlacedTile.smul_mk_mk, DiscreteTiling.PlacedTile.ext_iff, DiscreteTiling.PlacedTile.coe_finite_iff, DiscreteTiling.PlacedTile.coe_mk_finite_iff, ext_iff, DiscreteTiling.PlacedTile.coe_nonempty_iff, DiscreteTiling.PlacedTile.coe_mk_mk, DiscreteTiling.PlacedTile.smul_mk_coe, DiscreteTiling.PlacedTile.coe_mk_nonempty_iff, DiscreteTiling.PlacedTile.coe_mk_coe, coe_mk
instCoeOutSet 📖	CompOp	—
instInhabited 📖	CompOp	—
instMembership 📖	CompOp	1 math math: mem_coe
symmetries 📖	CompOp	8 math math: DiscreteTiling.PlacedTile.ext_iff_of_preimage, DiscreteTiling.PlacedTile.ext_iff_of_exists, DiscreteTiling.PlacedTile.smul_mk_mk, DiscreteTiling.PlacedTile.ext_iff, ext_iff, DiscreteTiling.PlacedTile.coe_mk_mk, DiscreteTiling.PlacedTile.smul_mk_coe, DiscreteTiling.PlacedTile.coe_mk_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mk 📖	mathematical	—	carrier	—	—
ext 📖	—	carrier Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup symmetries	—	—	—
ext_iff 📖	mathematical	—	carrier Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup symmetries	—	ext
mem_coe 📖	mathematical	—	Set Set.instMembership carrier DiscreteTiling.Prototile instMembership	—	—

---

← Back to Index