instIsStableUnderCobaseChangeIndOfHasPushouts

English

The functor-ind property is stable under cobase change (pushout) when pushouts exist.

Русский

Свойство индукции сохраняется при конструировании по cobase change (pushout), если такие пуш-ауты существуют.

LaTeX

$$$ P.ind.IsStableUnderCobaseChange$ under [HasPushouts]\, :\ P.ind.IsStableUnderCobaseChange$$

Lean4

instance [P.IsStableUnderCobaseChange] [HasPushouts C] : P.ind.IsStableUnderCobaseChange :=
  by
  refine .mk' fun A B A' f g _ hf ↦ ?_
  rw [ind_iff_ind_underMk] at hf ⊢
  exact ind_underObj_pushout g hf

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