lt_sizeof_cons' — Mathlib

English

For any a and l, SizeOf of the pair (b, a) is smaller than SizeOf of cons'(a, l).

Русский

Для любого a и l, размер пары (b, a) меньше размера конструируемого списка cons'(a, l).

LaTeX

$$$\\operatorname{SizeOf.sizeOf}(\\langle b, a \\rangle) < \\operatorname{SizeOf.sizeOf}(\\text{Lists'.cons'}'(a,l))$$$

Lean4

theorem lt_sizeof_cons' {b} (a : Lists' α b) (l) :
    SizeOf.sizeOf (⟨b, a⟩ : Lists α) < SizeOf.sizeOf (Lists'.cons' a l) :=
  by
  simp only [Sigma.mk.sizeOf_spec, Lists'.cons'.sizeOf_spec, lt_add_iff_pos_right]
  apply sizeof_pos

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