Theorems · Definition · logic and foundations

FirstOrder.Language.Hom.domRestrict

{L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type u_1} →
      [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Hom M N → (p : L.Substructure M) → L.Hom (↥p) N

The restriction of a first-order hom to a substructure s ⊆ M gives a hom s → N.

Defined in

Mathlib.ModelTheory.Substructures

Cited by

2 results in Mathlib

Foundations

Depth 20 from the axioms · uses Quot.sound

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure