Theorems · Definition · logic and foundations

FirstOrder.Language.Prestructure.noConfusion

{P : Sort u} →
  {L : FirstOrder.Language} →
    {M : Type u_1} →
      {s : Setoid M} →
        {t : L.Prestructure s} →
          {L' : FirstOrder.Language} →
            {M' : Type u_1} →
              {s' : Setoid M'} →
                {t' : L'.Prestructure s'} →
                  L = L' → M = M' → s ≍ s' → t ≍ t' → FirstOrder.Language.Prestructure.noConfusionType P t t'

Defined in

Mathlib.ModelTheory.Quotients

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms