lookupFinsupp_eq_zero_iff — Mathlib

English

The value at a under lookupFinsupp is zero exactly when either a is absent or the stored value is zero.

Русский

Значение в позиции $a$ у lookupFinsupp равно нулю тогда и только тогда, когда либо элемента нет, либо сохранённое значение равно нулю.

LaTeX

$$$l.lookupFinsupp(a) = 0 \\iff a \\notin l \\lor 0 \\in l.lookup a$$$

Lean4

theorem lookupFinsupp_eq_zero_iff [DecidableEq α] {l : AList fun _x : α => M} {a : α} :
    l.lookupFinsupp a = 0 ↔ a ∉ l ∨ (0 : M) ∈ l.lookup a :=
  by
  rw [lookupFinsupp_apply, ← lookup_eq_none]
  rcases lookup a l with - | m <;> simp

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