English
If β is finite, then HasProd f (∏_{b ∈ L.support} f(b)) L, provided L.HasSupport and decidability holds.
Русский
Если β конечно, то HasProd f (произведение по L.support) L при условии HasSupport иDecidable.
LaTeX
$$$ HasProd f (\prod_{b \in L.support} f b) L $ under Finite β and HasSupport$$
Lean4
@[to_additive]
theorem hasProd_fintype_support [Fintype β] (f : β → α) (L : SummationFilter β) [L.HasSupport]
[DecidablePred (· ∈ L.support)] : HasProd f (∏ b ∈ L.support, f b) L :=
by
apply tendsto_nhds_of_eventually_eq
have h1 : ⋂ b ∈ L.support, {s | b ∈ s} ∈ L.filter := (L.filter.biInter_mem L.support.toFinite).mpr (by tauto)
have h2 : ⋂ b ∈ L.supportᶜ, {s | b ∉ s} ∈ L.filter :=
(L.filter.biInter_mem L.supportᶜ.toFinite).mpr (fun b hb ↦ (L.eventually_mem_or_not_mem b).resolve_left hb)
filter_upwards [h1, h2] with s hs hs'
congr 1
simp only [Set.mem_iInter, Set.mem_setOf_eq, Set.mem_compl_iff] at hs hs'
grind [Set.mem_toFinset]
