faithful_exists — Mathlib

English

Let C be a category with images. For any morphism f: X → Y, the forward-subobject construction exists f : MonoOver X → MonoOver Y is a faithful functor.

Русский

Пусть C имеет образы. Для любого морфизма f: X → Y соответствующий функтор существует f : MonoOver X → MonoOver Y является верным (фидельным).

LaTeX

$$$\forall X,Y\ (f:X\to Y),\ \mathrm{Faithful}(\mathrm{exists}(f)).$$$

Lean4

instance faithful_exists (f : X ⟶ Y) : Functor.Faithful («exists» f) where

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