exists_blsub_cof — Mathlib

English

There exists f such that o.cof.ord.blsub f = o, with f defined below cof o.

Русский

Существует f such that o.cof.ord.blsub f = o, где f определяется ниже cof o.

LaTeX

$$$\\exists f:\\forall a < (\\operatorname{cof}(o)).ord, \\operatorname{Ordinal},\\ blsub(o,f)=o.$$$

Lean4

theorem exists_blsub_cof (o : Ordinal) : ∃ f : ∀ a < (cof o).ord, Ordinal, blsub.{u, u} _ f = o :=
  by
  rcases exists_lsub_cof o with ⟨ι, f, hf, hι⟩
  rcases Cardinal.ord_eq ι with ⟨r, hr, hι'⟩
  rw [← @blsub_eq_lsub' ι r hr] at hf
  rw [← hι, hι']
  exact ⟨_, hf⟩

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