epi_f₂₄ — Mathlib

English

In a pushout square, if the left vertical arrow f₁₃ is epimorphic, then the right vertical arrow f₂₄ is epimorphic.

Русский

В квадрате пуш-аут, если левая вертикальная стрелка f₁₃ является эпиморфизмом, то правая вертикальная стрелка f₂₄ также является эпиморфизмом.

LaTeX

$$$\operatorname{IsPushout}(sq) \;\wedge\; \operatorname{Epi}(sq.f_{13}) \Rightarrow \operatorname{Epi}(sq.f_{24})$$$

Lean4

theorem epi_f₂₄ [Epi sq.f₁₃] : Epi sq.f₂₄ :=
  (MorphismProperty.epimorphisms C).of_isPushout h (by assumption)

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