tprod_eqOn — Mathlib

English

For a T2 space α, if HasProdUniformlyOn f g 𝔖 and hs ∈ 𝔖, then on s the infinite product ∏' b, f b · equals g.

Русский

Для пространства T2 α, если HasProdUniformlyOn f g 𝔖 и hs ∈ 𝔖, тогда на s бесконечное произведение ∏' b, f b · равно g.

LaTeX

$$$ [T2Space\ α]\ (h : HasProdUniformlyOn f g 𝔖) (hs : s ∈ 𝔖) : s.EqOn (∏' b, f b ·) g $$$

Lean4

@[to_additive]
theorem tprod_eqOn [T2Space α] (h : HasProdUniformlyOn f g 𝔖) (hs : s ∈ 𝔖) : s.EqOn (∏' b, f b ·) g := fun _ hx ↦
  (h.hasProd hs hx).tprod_eq

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