Theorems · Theorem · logic and foundations

FirstOrder.Language.Substructure.mk.sizeOf_spec

∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] [inst_1 : SizeOf M] (carrier : Set M)
  (fun_mem : ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f carrier),
  sizeOf { carrier := carrier, fun_mem := fun_mem } = 1

Defined in

Mathlib.ModelTheory.Substructures

Cited by

0 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

FirstOrder.Language.StructureSizeOf