English
For b ∈ β, (p.bindOnSupport f)(b) equals zero if and only if for all a with p(a) ≠ 0, f(a, ha)(b) = 0.
Русский
Для b ∈ β, (p.bindOnSupport f)(b) равно нулю тогда и только тогда, когда для всех a с p(a) ≠ 0, f(a, ha)(b) = 0.
LaTeX
$$$$ (p.bindOnSupport f)(b) = 0 \\iff \\forall a, (p(a) \\neq 0) \\Rightarrow f(a, ha)(b) = 0 $$$$
Lean4
theorem bindOnSupport_eq_zero_iff (b : β) : p.bindOnSupport f b = 0 ↔ ∀ (a) (ha : p a ≠ 0), f a ha b = 0 :=
by
simp only [bindOnSupport_apply, ENNReal.tsum_eq_zero, mul_eq_zero, or_iff_not_imp_left]
exact ⟨fun h a ha => Trans.trans (dif_neg ha).symm (h a ha), fun h a ha => Trans.trans (dif_neg ha) (h a ha)⟩