cof_univ — Mathlib

English

cof univ = univ: the cofinality of the universal type equals the universal cardinal.

Русский

cof univ = univ: кофинальность универсума равна мощности универсума.

LaTeX

$$$$ \operatorname{cof}(\mathrm{univ}) = \mathrm{univ} $$$$

Lean4

@[simp]
theorem cof_univ : cof univ.{u, v} = Cardinal.univ.{u, v} :=
  le_antisymm (cof_le_card _)
    (by
      refine le_of_forall_lt fun c h => ?_
      rcases lt_univ'.1 h with ⟨c, rfl⟩
      rcases @cof_eq Ordinal.{u} (· < ·) _ with ⟨S, H, Se⟩
      rw [univ, ← lift_cof, ← Cardinal.lift_lift.{u + 1, v, u}, Cardinal.lift_lt, ← Se]
      refine lt_of_not_ge fun h => ?_
      obtain ⟨a, e⟩ := Cardinal.mem_range_lift_of_le h
      refine Quotient.inductionOn a (fun α e => ?_) e
      obtain ⟨f⟩ := Quotient.exact e
      have f := Equiv.ulift.symm.trans f
      let g a := (f a).1
      let o := succ (iSup g)
      rcases H o with ⟨b, h, l⟩
      refine l (lt_succ_iff.2 ?_)
      rw [← show g (f.symm ⟨b, h⟩) = b by simp [g]]
      apply Ordinal.le_iSup)

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