cof_cof — Mathlib

English

Same transitivity property for fundamental sequences as above (second formulation).

Русский

Та же сводимость для фундаментальных последовательностей во второй формулировке.

LaTeX

$$$$\text{IsFundamentalSequence}(a,o,f) \Rightarrow \text{IsFundamentalSequence}(a,o',f'), $$$$

Lean4

@[simp]
theorem cof_cof (a : Ordinal.{u}) : cof (cof a).ord = cof a :=
  by
  obtain ⟨f, hf⟩ := exists_fundamental_sequence a
  obtain ⟨g, hg⟩ := exists_fundamental_sequence a.cof.ord
  exact ord_injective (hf.trans hg).cof_eq.symm

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