Theorems · Definition · combinatorics

DiscreteTiling.PlacedTile.noConfusion

{P : Sort u} →
  {G : Type u_1} →
    {X : Type u_2} →
      {ιₚ : Type u_3} →
        {inst : Group G} →
          {inst_1 : MulAction G X} →
            {ps : DiscreteTiling.Protoset G X ιₚ} →
              {t : DiscreteTiling.PlacedTile ps} →
                {G' : Type u_1} →
                  {X' : Type u_2} →
                    {ιₚ' : Type u_3} →
                      {inst' : Group G'} →
                        {inst'_1 : MulAction G' X'} →
                          {ps' : DiscreteTiling.Protoset G' X' ιₚ'} →
                            {t' : DiscreteTiling.PlacedTile ps'} →
                              G = G' →
                                X = X' →
                                  ιₚ = ιₚ' →
                                    inst ≍ inst' →
                                      inst_1 ≍ inst'_1 →
                                        ps ≍ ps' → t ≍ t' → DiscreteTiling.PlacedTile.noConfusionType P t t'

Defined in

Mathlib.Combinatorics.Tiling.Tile

Cited by

0 results in Mathlib

Foundations

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