instFaithfulObjPost — Mathlib

English

If F is faithful, then the post construction is faithful on objects.

Русский

Если F верный (faithful), то построение поста для объектов сохраняет верность.

LaTeX

$$$\\operatorname{Faithful}(F) \\Rightarrow \\operatorname{Faithful}(\\mathrm{Over.post}\\ (X:=X)\, F)$$$

Lean4

instance [F.Faithful] : (Over.post (X := X) F).Faithful where
  map_injective {A B} f g
    h := by
    ext
    exact F.map_injective (congrArg CommaMorphism.left h)

Похожие утверждения