isAccessible_of_isCardinalAccessible

English

If F is κ-cardinally accessible for κ, then F is an accessible functor: there exists a κ such that F is κ-accessible.

Русский

Если F обладает κ-кардинальной доступностью, то F является доступным функтором: существует κ, при котором F является κ-доступным.

LaTeX

$$$[F.IsCardinalAccessible \kappa] \Rightarrow IsAccessible.F\text{ (with witness } \kappa)$$$

Lean4

theorem isAccessible_of_isCardinalAccessible (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalAccessible F κ] :
    IsAccessible.{w} F where exists_cardinal := ⟨κ, inferInstance, inferInstance⟩

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