sizeOf_kerase — Mathlib

English

If a ∈ l (with nodup keys), then a is not present in (kerase a l).keys. Erasing a from the list removes its key from the key-set.

Русский

Если ключ a присутствует в l с безповторными ключами, то a не принадлежит (kerase a l).keys.

LaTeX

$$∀ {l : List (Σ β)}, l.NodupKeys → a ∉ (kerase a l).keys$$

Lean4

theorem sizeOf_kerase [SizeOf (Sigma β)] (x : α) (xs : List (Sigma β)) :
    SizeOf.sizeOf (List.kerase x xs) ≤ SizeOf.sizeOf xs :=
  by
  simp only [SizeOf.sizeOf, _sizeOf_1]
  induction xs with
  | nil => simp
  | cons y ys => by_cases x = y.1 <;> simp [*]

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