Theorems · Theorem · logic and foundations

FirstOrder.Language.Substructure.mk.injEq

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

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext

Assumes

FirstOrder.Language.Structure