cof_type_le — Mathlib

English

If r is a well-order on α, then cof(type r) is bounded by the size of any unbounded subset S.

Русский

Если r определено как хорошо упорядоченное на α, то cof(type r) ограничено размером любого неабсолютно неограниченного подмножества S.

LaTeX

$$$\\text{cof\_type} \\le |S|$ for unbounded S$$

Lean4

theorem cof_type_le [IsWellOrder α r] {S : Set α} (h : Unbounded r S) : cof (type r) ≤ #S :=
  le_cof_type.1 le_rfl S h

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