isCardinalAccessible_of_le — Mathlib

English

If F is κ-accessible and J is essentially small, then PreservesColimitsOfShape J F.

Русский

Если F доступен по κ и J существенно мал, тогда F сохраняет колимиты по форме J.

LaTeX

$$$[F.IsCardinalAccessible \kappa] \to [J\;\text{essentiallySmall}] \Rightarrow \text{PreservesColimitsOfShape } J F$$$

Lean4

theorem isCardinalAccessible_of_le [F.IsCardinalAccessible κ] {κ' : Cardinal.{w}} [Fact κ'.IsRegular] (h : κ ≤ κ') :
    F.IsCardinalAccessible κ' where
  preservesColimitOfShape
    {J _ _} := by
    have := IsCardinalFiltered.of_le J h
    exact F.preservesColimitsOfShape_of_isCardinalAccessible κ J

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