zero — Mathlib

English

The zero ordinal forms a trivial fundamental sequence: IsFundamentalSequence 0 0 f for any f with appropriate domain.

Русский

Нулевой порядок образует тривиальную фундаментальную последовательность: IsFundamentalSequence 0 0 f для любого допустимого f.

LaTeX

$$$$\text{IsFundamentalSequence}(0,0,f)$$$$

Lean4

protected theorem zero {f : ∀ b < (0 : Ordinal), Ordinal} : IsFundamentalSequence 0 0 f :=
  ⟨by rw [cof_zero, ord_zero], @fun i _ hi => (Ordinal.not_lt_zero i hi).elim, blsub_zero f⟩

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