Theorems · Theorem · logic and foundations

FirstOrder.Language.Substructure.mk.congr_simp

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

Defined in

Mathlib.ModelTheory.Substructures

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

FirstOrder.Language.Structure