Theorems · Definition · logic and foundations

FirstOrder.Language.Theory.CompleteType.mk.noConfusion

{L : FirstOrder.Language} →
  {T : L.Theory} →
    {α : Type w} →
      {P : Sort u_1} →
        {toTheory : (L.withConstants α).Theory} →
          {subset' : (L.lhomWithConstants α).onTheory T ⊆ toTheory} →
            {isMaximal' : toTheory.IsMaximal} →
              {toTheory' : (L.withConstants α).Theory} →
                {subset'' : (L.lhomWithConstants α).onTheory T ⊆ toTheory'} →
                  {isMaximal'' : toTheory'.IsMaximal} →
                    { toTheory := toTheory, subset' := subset', isMaximal' := isMaximal' } =
                        { toTheory := toTheory', subset' := subset'', isMaximal' := isMaximal'' } →
                      (toTheory ≍ toTheory' → P) → P

Defined in

Mathlib.ModelTheory.Types

Cited by

1 results in Mathlib

Foundations

Depth 24 from the axioms · uses no axioms