English
For a finite set s, if all indices outside s contribute at least 1, then the finite product over s is bounded by the HasProd bound a.
Русский
Для конечного множества s, если все индексы вне s дают не менее 1, то произведение по s не превосходит верхнюю грань a HasProd.
LaTeX
$$$\\forall s:\\, Finset\\ ι,\\ (\\forall i\\notin s, 1 \\le f i)\\to \\text{HasProd } f\\ a\\ L\\to \\left(\\prod_{i\\in s} f(i)\\right) \\le a$$$
Lean4
@[to_additive]
theorem prod_le_hasProd [L.NeBot] [L.LeAtTop] (s : Finset ι) (hs : ∀ i, i ∉ s → 1 ≤ f i) (hf : HasProd f a L) :
∏ i ∈ s, f i ≤ a :=
by
refine ge_of_tendsto hf <| .filter_mono L.le_atTop <| eventually_atTop.2 ?_
exact ⟨s, fun _t hst ↦ prod_le_prod_of_subset_of_one_le' hst fun i _ hbs ↦ hs i hbs⟩
