mono_iff_mono_right — Mathlib

English

In a structured-arrow setting with pullbacks, Mono f if and only if Mono f.right.

Русский

В условиях структурированной стрелки с притяжениями: Mono f тогда и только тогда, когда Mono f.right.

LaTeX

$$$\\text{Mono}(f) \\iff \\text{Mono}(f.right)$$$

Lean4

theorem mono_iff_mono_right [HasPullbacks A] [PreservesLimitsOfShape WalkingCospan G] {Y Z : StructuredArrow X G}
    (f : Y ⟶ Z) : Mono f ↔ Mono f.right :=
  ⟨fun _ => inferInstance, fun _ => mono_of_mono_right f⟩

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