le_cof_iff_blsub — Mathlib

English

Characterizes a ≤ cof b via all b-substructures Blsub representations: a ≤ cof b iff for every o and f with o.blsub f = b we have a ≤ o.card.

Русский

Характеризует неравенство a ≤ cof b через все представления b как o.blsub f: a ≤ cof b тогда и только тогда, когда для каждого o и f с o.blsub f = b выполняется a ≤ o.card.

LaTeX

$$$a \\le \\operatorname{cof}(b) \\iff \\forall {o} (f: \\forall a

Lean4

theorem le_cof_iff_blsub {b : Ordinal} {a : Cardinal} :
    a ≤ cof b ↔ ∀ {o} (f : ∀ a < o, Ordinal), blsub.{u, u} o f = b → a ≤ o.card :=
  le_cof_iff_lsub.trans
    ⟨fun H o f hf => by simpa using H _ hf, fun H ι f hf =>
      by
      rcases Cardinal.ord_eq ι with ⟨r, hr, hι'⟩
      rw [← @blsub_eq_lsub' ι r hr] at hf
      simpa using H _ hf⟩

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