preservesColimitsOfShape_of_isCardinalAccessible

English

If F is κ-cardinally accessible, then for any κ ≤ κ' with κ' regular, F is κ'-cardinally accessible; equivalently, preserves more colimits along larger shapes.

Русский

Если F обладает κ-кардинальной доступностью, то при любом κ ≤ κ' с κ' регулярным, F обладает κ'-кардинальной доступностью; то есть сохраняет больше колимит на более широких формах.

LaTeX

$$$[F.IsCardinalAccessible\;\kappa] \Rightarrow [\kappa \le \kappa' \Rightarrow F.IsCardinalAccessible \; \kappa']$$$

Lean4

theorem preservesColimitsOfShape_of_isCardinalAccessible [F.IsCardinalAccessible κ] (J : Type w) [SmallCategory J]
    [IsCardinalFiltered J κ] : PreservesColimitsOfShape J F :=
  IsCardinalAccessible.preservesColimitOfShape κ _

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