Theorems · Definition · logic and foundations

FirstOrder.Language.LHom.substructureReduct

{L : FirstOrder.Language} →
  {M : Type w} →
    [inst : L.Structure M] →
      {L' : FirstOrder.Language} →
        [inst_1 : L'.Structure M] → (φ : L →ᴸ L') → [φ.IsExpansionOn M] → L'.Substructure M ↪o L.Substructure M

Reduces the language of a substructure along a language hom.

Defined in

Mathlib.ModelTheory.Substructures

Cited by

6 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Quot.sound

Assumes

FirstOrder.Language.StructureFirstOrder.Language.StructureFirstOrder.Language.LHom.IsExpansionOn