sizeOf_lt_sizeOf_of_mem — Mathlib

English

If x is an element of a finite list l in a type with a SizeOf structure, then the size of x is strictly less than the size of l.

Русский

Если x ∈ l, где l конечен, в типе с размером SizeOf, то SizeOf x < SizeOf l.

LaTeX

$$$$\forall x\in l:\; \operatorname{sizeOf}(x) < \operatorname{sizeOf}(l).$$$$

Lean4

@[deprecated "Deprecated without replacement." (since := "2025-02-07")]
theorem sizeOf_lt_sizeOf_of_mem [SizeOf α] {x : α} {l : List α} (hx : x ∈ l) : SizeOf.sizeOf x < SizeOf.sizeOf l :=
  by
  induction l with
      | nil => ?_
      | cons h t ih => ?_ <;>
      cases hx <;>
    rw [cons.sizeOf_spec]
  · cutsat
  · specialize ih ‹_›
    cutsat

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