Theorems · Theorem · logic and foundations

FirstOrder.Language.Theory.CompleteType.mk.injEq

∀ {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

0 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext