mono_of_isLimit_parallelFamily — Mathlib

English

A wide equalizer map ι f is a monomorphism.

Русский

Гомоморфизм широкого эквалайзера ι f является мономорфизмом.

LaTeX

$$$\text{Mono}(wideEqualizer.ι f)$$$

Lean4

/-- The wide equalizer morphism in any limit cone is a monomorphism. -/
theorem mono_of_isLimit_parallelFamily [Nonempty J] {c : Cone (parallelFamily f)} (i : IsLimit c) : Mono (Trident.ι c)
    where right_cancellation _ _ w := Trident.IsLimit.hom_ext i w

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