Theorems · Theorem · logic and foundations

FirstOrder.Language.LHom.mk.injEq

∀ {L : FirstOrder.Language} {L' : FirstOrder.Language}
  (onFunction : autoParam (⦃n : ℕ⦄ → L.Functions n → L'.Functions n) FirstOrder.Language.LHom.onFunction._autoParam)
  (onRelation : autoParam (⦃n : ℕ⦄ → L.Relations n → L'.Relations n) FirstOrder.Language.LHom.onRelation._autoParam)
  (onFunction_1 : autoParam (⦃n : ℕ⦄ → L.Functions n → L'.Functions n) FirstOrder.Language.LHom.onFunction._autoParam)
  (onRelation_1 : autoParam (⦃n : ℕ⦄ → L.Relations n → L'.Relations n) FirstOrder.Language.LHom.onRelation._autoParam),
  ({ onFunction := onFunction, onRelation := onRelation } =
      { onFunction := onFunction_1, onRelation := onRelation_1 }) =
    (onFunction = onFunction_1 ∧ onRelation = onRelation_1)

Defined in

Mathlib.ModelTheory.LanguageMap

Cited by

1 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext