isCardinalPresentable_of_le — Mathlib

English

If X is κ-presentable and κ ≤ κ', then X is κ'-presentable.

Русский

Если X κ-представим, и κ ≤ κ', то X κ'-представим.

LaTeX

$$$[IsCardinalPresentable X \kappa] [\kappa \le \kappa'] \Rightarrow IsCardinalPresentable X \kappa'$$$

Lean4

theorem isCardinalPresentable_of_le [IsCardinalPresentable X κ] {κ' : Cardinal.{w}} [Fact κ'.IsRegular] (h : κ ≤ κ') :
    IsCardinalPresentable X κ' :=
  (coyoneda.obj (op X)).isCardinalAccessible_of_le h

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