Theorems · Definition · logic and foundations

FirstOrder.Language.Embedding.codRestrict

{L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type u_1} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          (p : L.Substructure N) → (f : L.Embedding M N) → (∀ (c : M), f c ∈ p) → L.Embedding M ↥p

A first-order embedding f : M → N whose values lie in a substructure p ⊆ N can be restricted to an embedding M → p.

Defined in

Mathlib.ModelTheory.Substructures

Cited by

6 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure