sizeOf_dedupKeys — Mathlib

English

The size of the deduplicated keys is no greater than the size of the original list; equivalently, the size measure decreases under deduplication.

Русский

Размер dedupKeys не превосходит размера исходного списка.

LaTeX

$$SizeOf.sizeOf (dedupKeys l) ≤ SizeOf.sizeOf l$$

Lean4

theorem sizeOf_dedupKeys [SizeOf (Sigma β)] (xs : List (Sigma β)) : SizeOf.sizeOf (dedupKeys xs) ≤ SizeOf.sizeOf xs :=
  by
  simp only [SizeOf.sizeOf, _sizeOf_1]
  induction xs with
  | nil => simp [dedupKeys]
  | cons x xs =>
    simp only [dedupKeys_cons, kinsert_def, Nat.add_le_add_iff_left, Sigma.eta]
    trans
    · apply sizeOf_kerase
    · assumption

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