instIsStableUnderCobaseChangeMonomorphismsType

English

The class of monomorphisms in Type u is stable under cobase change.

Русский

Класс мономорфизмов в Type u устойчив к базовым изменениям (каскадам надворных изменений).

LaTeX

$$$ (\\text{monomorphisms }(\\mathrm{Type}\\, u)).IsStableUnderCobaseChange $$$

Lean4

instance : (monomorphisms (Type u)).IsStableUnderCobaseChange where
  of_isPushout {X₁ X₂ X₃ X₄ t l r b} sq
    ht := by
    simp only [monomorphisms.iff] at ht ⊢
    exact Limits.Types.pushoutCocone_inr_mono_of_isColimit sq.flip.isColimit

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