Theorems · Theorem · logic and foundations

FirstOrder.Language.Theory.CompleteType.mk.inj

∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {toTheory : (L.withConstants α).Theory}
  {subset' : (L.lhomWithConstants α).onTheory T ⊆ toTheory} {isMaximal' : toTheory.IsMaximal}
  {toTheory_1 : (L.withConstants α).Theory} {subset'_1 : (L.lhomWithConstants α).onTheory T ⊆ toTheory_1}
  {isMaximal'_1 : toTheory_1.IsMaximal},
  { toTheory := toTheory, subset' := subset', isMaximal' := isMaximal' } =
      { toTheory := toTheory_1, subset' := subset'_1, isMaximal' := isMaximal'_1 } →
    toTheory = toTheory_1

Defined in

Mathlib.ModelTheory.Types

Cited by

1 results in Mathlib

Foundations

Depth 25 from the axioms · uses no axioms