cof_eq_zero — Mathlib

English

For any ordinal o, cof(o) = 0 if and only if o = 0.

Русский

Для любого порядка o cof(o)=0 тогда и только тогда, когда o=0.

LaTeX

$$$$\operatorname{cof}(o)=0 \iff o=0.$$$$

Lean4

@[simp]
theorem cof_eq_zero {o} : cof o = 0 ↔ o = 0 :=
  ⟨inductionOn o fun _ r _ z =>
      let ⟨_, hl, e⟩ := cof_eq r
      type_eq_zero_iff_isEmpty.2 <|
        ⟨fun a =>
          let ⟨_, h, _⟩ := hl a
          (mk_eq_zero_iff.1 (e.trans z)).elim' ⟨_, h⟩⟩,
    fun e => by simp [e]⟩

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