isCardinalAccessible_of_natIso — Mathlib

English

If F is κ-cardinally accessible and e: F ≅ G, then G is κ-cardinally accessible.

Русский

Если F обладает κ-кардинальной доступностью и e: F ≅ G, то G обладает κ-кардинальной доступностью.

LaTeX

$$$[F.IsCardinalAccessible\kappa] \Rightarrow [\text{NatIso } e: F \simeq G] \Rightarrow G.IsCardinalAccessible\kappa$$$

Lean4

theorem isCardinalAccessible_of_natIso [F.IsCardinalAccessible κ] : G.IsCardinalAccessible κ where
  preservesColimitOfShape J _
    hκ := by
    have := F.preservesColimitsOfShape_of_isCardinalAccessible κ J
    exact preservesColimitsOfShape_of_natIso e

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