mono_of_isPushout_of_mono_right — Mathlib

English

If a square is a pushout, and the right-hand morphism g is mono, then the left-most morphism f is mono and the top-right morphism h is mono.

Русский

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

LaTeX

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

Lean4

theorem mono_of_isPushout_of_mono_right [Adhesive C] (H : IsPushout f g h i) [Mono g] : Mono h :=
  (Adhesive.van_kampen' H).mono_of_mono_right

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