bindOnSupport_eq_zero_iff — Mathlib

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)⟩

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