Theorems · Theorem · logic and foundations

FirstOrder.Language.withConstants_funMap_sumInr

∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] (α : Type u_1)
  [inst_1 : (FirstOrder.Language.constantsOn α).Structure M] {a : α} {x : Fin 0 → M},
  FirstOrder.Language.Structure.funMap (Sum.inr a) x = ↑(L.con a)

Defined in

Mathlib.ModelTheory.LanguageMap

Cited by

1 results in Mathlib

Foundations

Depth 19 from the axioms · uses Quot.sound

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure