sizeof_pos — Mathlib

English

For any l in Lists' α b, the size of l is strictly positive: 0 < SizeOf.sizeOf l.

Русский

Для любого l в Lists' α b размер l строго положителен: 0 < SizeOf.sizeOf l.

LaTeX

$$$0 < \\operatorname{SizeOf.sizeOf}(l)$$$

Lean4

theorem sizeof_pos {b} (l : Lists' α b) : 0 < SizeOf.sizeOf l := by
  cases l <;>
    simp only [Lists'.atom.sizeOf_spec, Lists'.nil.sizeOf_spec, Lists'.cons'.sizeOf_spec, true_or, add_pos_iff,
      zero_lt_one]

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