tprod_of_exists_eq_zero — Mathlib

English

If there exists b with f(b) = 0 and the usual topological hypotheses hold, then the tprod ∏' b, f b equals 0.

Русский

Если существует b такое, что f(b) = 0 и выполняются обычные топологические гипотезы, то tprod ∏' b f(b) = 0.

LaTeX

$$$[T2Space α] [L.NeBot] [L.LeAtTop] (hf : ∃ b, f b = 0) : ∏'[L] b, f b = 0$$$

Lean4

theorem tprod_of_exists_eq_zero [T2Space α] [L.NeBot] [L.LeAtTop] (hf : ∃ b, f b = 0) : ∏'[L] b, f b = 0 :=
  (hasProd_zero_of_exists_eq_zero hf).tprod_eq

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