isWellOrderContinuous_of_iso — Mathlib

English

If F ≅ G and F is well-order-continuous, then G is also well-order-continuous.

Русский

Если F изоморфно G и F хорошо-упорядоченно непрерывна, то и G тоже хорошо-упорядоченно непрерывна.

LaTeX

$$$\text{IsWellOrderContinuous}(F) \Rightarrow \text{IsWellOrderContinuous}(G)$ for an isomorphism $F \cong G$$$

Lean4

theorem isWellOrderContinuous_of_iso {F G : J ⥤ C} (e : F ≅ G) [F.IsWellOrderContinuous] : G.IsWellOrderContinuous where
  nonempty_isColimit (m : J)
    (hm :
      Order.IsSuccLimit
        m) :=
    ⟨(IsColimit.precomposeHomEquiv (isoWhiskerLeft _ e) _).1
        (IsColimit.ofIsoColimit (F.isColimitOfIsWellOrderContinuous m hm) (Cocones.ext (e.app _)))⟩

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