mk_eq_bot_iff_zero — Mathlib

English

For any f: X → Y that is mono, Subobject.mk f equals ⊥ if and only if f = 0.

Русский

Для монофункции f: X → Y подпорядок Subobjectmk f равен ⊥ тогда и только тогда, когда f = 0.

LaTeX

$$$ Subobject.mk f = \\bot \\iff f = 0 $$$

Lean4

theorem mk_eq_bot_iff_zero {f : X ⟶ Y} [Mono f] : Subobject.mk f = ⊥ ↔ f = 0 :=
  ⟨fun h => by simpa [h, bot_factors_iff_zero] using mk_factors_self f, fun h =>
    mk_eq_mk_of_comm _ _ ((isoZeroOfMonoEqZero h).trans HasZeroObject.zeroIsoInitial) (by simp [h])⟩

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