English
If a finite collection of elements all lie in the unit interval, then their product lies in the unit interval.
Русский
Если у конечного числа элементов каждое из которых лежит в единичном интервале, их произведение тоже лежит в единичном интервале.
LaTeX
$$∀ finite t and f : t → ℝ, (∀c ∈ t, f c ∈ [0,1]) → ∏_{c ∈ t} f c ∈ [0,1].$$
Lean4
protected theorem prod_mem {ι : Type*} {t : Finset ι} {f : ι → ℝ} (h : ∀ c ∈ t, f c ∈ unitInterval) :
∏ c ∈ t, f c ∈ unitInterval :=
_root_.prod_mem (S := unitInterval.submonoid) h