isomorphisms — Mathlib

English

If the property P holds for all isomorphisms, then it is stable under cobase change for all isomorphisms.

Русский

Если свойство P выполняется для всех изоморфизмов, то оно стабильно по cobase change для всех изоморфизмов.

LaTeX

$$IsStableUnderCobaseChange.forIsomorphisms(P) : (isomorphisms C).IsStableUnderCobaseChange$$

Lean4

instance isomorphisms : (isomorphisms C).IsStableUnderCobaseChange where
  of_isPushout {_ _ _ _ f g _ _} h
    (_ : IsIso f) :=
    have := hasPushout_of_right_iso g f
    h.inl_isoPushout_inv ▸ inferInstanceAs (IsIso _)

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