Theorems · Theorem · combinatorics

DiscreteTiling.PlacedTile.ext_iff_of_preimage

∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} {pt₁ pt₂ : DiscreteTiling.PlacedTile ps},
  pt₁ = pt₂ ↔
    pt₁.index = pt₂.index ∧
      Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₁.index)).subtype (↑ps pt₁.index).symmetries)) ⁻¹'
          {pt₁.groupElts} =
        Quotient.mk
            (QuotientGroup.leftRel
              (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₂.index)).subtype (↑ps pt₂.index).symmetries)) ⁻¹'
          {pt₂.groupElts}

An alternative extensionality principle for PlacedTile that avoids HEq, using equality of quotient preimages.

Defined in

Mathlib.Combinatorics.Tiling.Tile

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupMulAction