Theorems · Definition · combinatorics

DiscreteTiling.Prototile.noConfusion

{P : Sort u} →
  {G : Type u_1} →
    {X : Type u_2} →
      {inst : Group G} →
        {inst_1 : MulAction G X} →
          {t : DiscreteTiling.Prototile G X} →
            {G' : Type u_1} →
              {X' : Type u_2} →
                {inst' : Group G'} →
                  {inst'_1 : MulAction G' X'} →
                    {t' : DiscreteTiling.Prototile G' X'} →
                      G = G' →
                        X = X' →
                          inst ≍ inst' → inst_1 ≍ inst'_1 → t ≍ t' → DiscreteTiling.Prototile.noConfusionType P t t'

Defined in

Mathlib.Combinatorics.Tiling.Tile

Cited by

0 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Quot.sound