English
If F is κ-cardinally accessible and e: F ≅ G is a natural isomorphism, 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 preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall [F.IsCardinalAccessible κ] (J : Type u₃)
[Category.{v₃} J] [EssentiallySmall.{w} J] [IsCardinalFiltered J κ] : PreservesColimitsOfShape J F :=
by
have := IsCardinalFiltered.of_equivalence κ (equivSmallModel.{w} J)
have := F.preservesColimitsOfShape_of_isCardinalAccessible κ (SmallModel.{w} J)
exact preservesColimitsOfShape_of_equiv (equivSmallModel.{w} J).symm F
