English
For a sigma-type decomposition, the HasProd of a function on Σ b γ b equals the HasProd of the corresponding fiberwise products.
Русский
Для сигмоидального разложения имеет место равенство HasProd на σ‑типа равен HasProd для соответствующих волоконных произведений.
LaTeX
$$$\\forall γ, f : (Σ b, γ b) → α, g : β → α, a, (ha : HasProd f a) \\Rightarrow (\\forall b, HasProd (λ c, f (⟨b,c⟩)) (g b)) → HasProd g a$$$
Lean4
@[to_additive]
theorem sigma {γ : β → Type*} {f : (Σ b : β, γ b) → α} {g : β → α} {a : α} (ha : HasProd f a)
(hf : ∀ b, HasProd (fun c ↦ f ⟨b, c⟩) (g b)) : HasProd g a := by
classical
refine (atTop_basis.tendsto_iff (closed_nhds_basis a)).mpr ?_
rintro s ⟨hs, hsc⟩
rcases mem_atTop_sets.mp (ha hs) with ⟨u, hu⟩
use u.image Sigma.fst, trivial
intro bs hbs
simp only [Set.mem_preimage, Finset.le_iff_subset] at hu
have : Tendsto (fun t : Finset (Σ b, γ b) ↦ ∏ p ∈ t with p.1 ∈ bs, f p) atTop (𝓝 <| ∏ b ∈ bs, g b) :=
by
simp only [← sigma_preimage_mk, prod_sigma]
refine tendsto_finset_prod _ fun b _ ↦ ?_
change Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
refine hsc.mem_of_tendsto this (eventually_atTop.2 ⟨u, fun t ht ↦ hu _ fun x hx ↦ ?_⟩)
exact mem_filter.2 ⟨ht hx, hbs <| mem_image_of_mem _ hx⟩
