tprod_eq — Mathlib

English

If the union of the sets in 𝔖 is the entire space, then the infinite product ∏' b, f b · equals g.

Русский

Если объединение множеств 𝔖 охватывает всю область, то бесконечное произведение ∏' b, f b · равно g.

LaTeX

$$$ [T2Space\ α]\ (h : HasProdUniformlyOn f g 𝔖) (hs : ⋃₀ 𝔖 = Set.univ) : (∏' b, f b ·) = g $$$

Lean4

@[to_additive]
theorem tprod_eq [T2Space α] (h : HasProdUniformlyOn f g 𝔖) (hs : ⋃₀ 𝔖 = Set.univ) : (∏' b, f b ·) = g :=
  by
  ext x
  obtain ⟨s, hs, hx⟩ := by simpa [← hs] using Set.mem_univ x
  exact h.tprod_eqOn hs hx

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