Theorems · Theorem · logic and foundations

FirstOrder.Language.Hom.codRestrict_toFun_coe

∀ {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.Hom M N) (h : ∀ (c : M), f c ∈ p) (c : M),
  ↑((FirstOrder.Language.Hom.codRestrict p f h) c) = f c

Defined in

Mathlib.ModelTheory.Substructures

Cited by

0 results in Mathlib

Foundations

Depth 20 from the axioms · uses no axioms

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure