Theorems · Definition · logic and foundations

FirstOrder.Language.ElementarySubstructure.noConfusion

{P : Sort u} →
  {L : FirstOrder.Language} →
    {M : Type u_1} →
      {inst : L.Structure M} →
        {t : L.ElementarySubstructure M} →
          {L' : FirstOrder.Language} →
            {M' : Type u_1} →
              {inst' : L'.Structure M'} →
                {t' : L'.ElementarySubstructure M'} →
                  L = L' →
                    M = M' → inst ≍ inst' → t ≍ t' → FirstOrder.Language.ElementarySubstructure.noConfusionType P t t'

Defined in

Mathlib.ModelTheory.ElementarySubstructures

Cited by

0 results in Mathlib

Foundations

Depth 27 from the axioms · uses Quot.sound