lookupFinsupp_eq_iff_of_ne_zero — Mathlib

English

If x ≠ 0, then l.lookupFinsupp a = x iff x ∈ l.lookup a.

Русский

Пусть $x \\neq 0$. Тогда $l.lookupFinsupp(a)=x$ тогда и только тогда, когда $x \\in l.lookup(a)$.

LaTeX

$$$\\text{If } x \\neq 0, \\quad l.lookupFinsupp(a) = x \\iff x \\in l.lookup(a)$$$

Lean4

theorem lookupFinsupp_eq_iff_of_ne_zero [DecidableEq α] {l : AList fun _x : α => M} {a : α} {x : M} (hx : x ≠ 0) :
    l.lookupFinsupp a = x ↔ x ∈ l.lookup a := by
  rw [lookupFinsupp_apply]
  rcases lookup a l with - | m <;> simp [hx.symm]

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