Theorems · Definition · logic and foundations

FirstOrder.Language.Substructure.noConfusion

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

Defined in

Mathlib.ModelTheory.Substructures

Cited by

0 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms