cof_succ — Mathlib

English

The cofinality of a successor ordinal is 1: cof(succ o) = 1.

Русский

Кофинальность последовательного числа равна 1: cof(succ o) = 1.

LaTeX

$$$$\operatorname{cof}(\operatorname{succ} o)=1.$$$$

Lean4

@[simp]
theorem cof_succ (o) : cof (succ o) = 1 := by
  apply le_antisymm
  · refine inductionOn o fun α r _ => ?_
    change cof (type _) ≤ _
    rw [← (_ : #_ = 1)]
    · apply cof_type_le
      refine fun a => ⟨Sum.inr PUnit.unit, Set.mem_singleton _, ?_⟩
      rcases a with (a | ⟨⟨⟨⟩⟩⟩) <;> simp [EmptyRelation]
    · simp
  · rw [← Cardinal.succ_zero, succ_le_iff]
    simpa [lt_iff_le_and_ne, Cardinal.zero_le] using fun h => succ_ne_zero o (cof_eq_zero.1 (Eq.symm h))

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