Theorems · Definition · logic and foundations

FirstOrder.Language.Substructure.comap

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

The preimage of a substructure along a homomorphism is a substructure.

Defined in

Mathlib.ModelTheory.Substructures

Cited by

31 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure