Theorems · Theorem · logic and foundations

FirstOrder.Language.Theory.CompleteType.mk.sizeOf_spec

∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} [inst : (a : L.Sentence) → SizeOf (T a)] [inst_1 : SizeOf α]
  (toTheory : (L.withConstants α).Theory) (subset' : (L.lhomWithConstants α).onTheory T ⊆ toTheory)
  (isMaximal' : toTheory.IsMaximal),
  sizeOf { toTheory := toTheory, subset' := subset', isMaximal' := isMaximal' } = 1 + sizeOf isMaximal'

Defined in

Mathlib.ModelTheory.Types

Cited by

0 results in Mathlib

Foundations

Depth 23 from the axioms · uses no axioms

Assumes

SizeOfSizeOf