English
Definition: HasProdLocallyUniformlyOn f g s holds if the finite products ∏ i∈I f i b converge locally uniformly on s to g(b).
Русский
Определение: HasProdLocallyUniformlyOn f g s означает, что локально по s на b произведения ∏ i∈I f i b сходятся равномерно по локализации к g(b).
LaTeX
$$$ HasProdLocallyUniformlyOn f g s := TendstoLocallyUniformlyOn (\lambda I b. \prod_{i∈I} f i b) g atTop s $$$
Lean4
/-- `HasProdLocallyUniformlyOn f g s` means that the (potentially infinite) product `∏' i, f i b`
for `b : β` converges locally uniformly on `s` to `g b` (in the sense of
`TendstoLocallyUniformlyOn`). -/
@[to_additive /-- `HasSumLocallyUniformlyOn f g s` means that the (potentially infinite) sum
`∑' i, f i b` for `b : β` converges locally uniformly on `s` to `g b` (in the sense of
`TendstoLocallyUniformlyOn`). -/
]
def HasProdLocallyUniformlyOn : Prop :=
TendstoLocallyUniformlyOn (fun I b ↦ ∏ i ∈ I, f i b) g atTop s
