mono_of_isPushout_of_mono_left — Mathlib

English

If a square is a pushout, and the left-hand morphism f is mono, then the far-right morphism i is mono.

Русский

Если квадрат является pushout, и левая стрелка f является моно, то правая стрелка i моно.

LaTeX

$$IsPushout(f,g,h,i) \rightarrow Mono(f) \rightarrow Mono(i)$$

Lean4

theorem mono_of_isPushout_of_mono_left [Adhesive C] (H : IsPushout f g h i) [Mono f] : Mono i :=
  (Adhesive.van_kampen H).mono_of_mono_left

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