isPresentable_of_isCardinalPresentable

English

If X is κ-presentable for some regular κ, then X is presentable.

Русский

Если X κ-представим для некоторого регулярного κ, тогда X представим.

LaTeX

$$$\text{IsPresentable}(X) \quad\text{from}\quad [IsCardinalPresentable X \kappa]$$$

Lean4

theorem isPresentable_of_isCardinalPresentable (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalPresentable X κ] :
    IsPresentable.{w} X where exists_cardinal := ⟨κ, inferInstance, inferInstance⟩

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