prod_mem — Mathlib

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

Похожие утверждения