Theorems · Theorem · logic and foundations

FirstOrder.Language.Substructure.mk.inj

∀ {L : FirstOrder.Language} {M : Type w} {inst : L.Structure M} {carrier : Set M}
  {fun_mem : ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f carrier} {carrier_1 : Set M}
  {fun_mem_1 : ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f carrier_1},
  { carrier := carrier, fun_mem := fun_mem } = { carrier := carrier_1, fun_mem := fun_mem_1 } → carrier = carrier_1

Defined in

Mathlib.ModelTheory.Substructures

Cited by

1 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms