le_cof_iff_lsub — Mathlib

English

For any o and a, a ≤ cof(o) if and only if every representation of o as lsub(f) has cardinality at least a.

Русский

Для любых o и a верно: a ≤ cof(o) тогда и только тогда, когда любая запись o = lsub(f) удовлетворяет a ≤ |ι|.

LaTeX

$$$a \\le \\operatorname{cof}(o) \\iff \\forall \\iota\\ , \\forall f:\\iota\\to \\operatorname{Ordinal},\\ \\operatorname{lsub}(f)=o \\Rightarrow a \\le \\#\\iota.$$$

Lean4

theorem le_cof_iff_lsub {o : Ordinal} {a : Cardinal} :
    a ≤ cof o ↔ ∀ {ι} (f : ι → Ordinal), lsub.{u, u} f = o → a ≤ #ι :=
  by
  rw [cof_eq_sInf_lsub]
  exact
    (le_csInf_iff'' (cof_lsub_def_nonempty o)).trans
      ⟨fun H ι f hf => H _ ⟨ι, f, hf, rfl⟩, fun H b ⟨ι, f, hf, hb⟩ =>
        by
        rw [← hb]
        exact H _ hf⟩

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