hasProd_zero_of_exists_eq_zero — Mathlib

English

If there exists b with f(b) = 0, then the HasProd f 0 with respect to a summation filter L holds, provided L is compatible with atTop.

Русский

Если существует b такое, что f(b) = 0, тогда HasProd f 0 существует относительно фильтра суммирования L (при условии совместимости с atTop).

LaTeX

$$$(\\exists b, f b = 0) \\Rightarrow HasProd f 0 L$$$

Lean4

theorem hasProd_zero_of_exists_eq_zero (hf : ∃ b, f b = 0) [L.LeAtTop] : HasProd f 0 L :=
  by
  obtain ⟨b, hb⟩ := hf
  apply tendsto_const_nhds.congr'
  filter_upwards [(eventually_ge_atTop { b }).filter_mono L.le_atTop] with s hs
  exact (Finset.prod_eq_zero (Finset.singleton_subset_iff.mp hs) hb).symm

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