lt_snd — Mathlib

English

Every coefficient in a Cantor normal form is positive; in particular the second component of each pair in CNF is positive.

Русский

Каждый коэффициент канторовской нормальной формы положителен; в частности вторая компонента пары положительна.

LaTeX

$$$\forall b\,\forall o\; x \in CNF(b, o) \Rightarrow 0 < x.2$$$

Lean4

/-- Every coefficient in a Cantor normal form is positive. -/
theorem lt_snd {b o : Ordinal.{u}} {x : Ordinal × Ordinal} : x ∈ CNF b o → 0 < x.2 :=
  by
  refine CNF.rec b (by simp) (fun o ho IH ↦ ?_) o
  rw [CNF.ne_zero ho]
  rintro (h | ⟨_, h⟩)
  · exact div_opow_log_pos b ho
  · exact IH h

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