prod — Mathlib

English

If a finite family {f i} indexed by s consists of left-regular elements, then the product over i∈s is left-regular.

Русский

Если конечная семейство элементов {f_i} индексировано множеством s состоит из левых регулярных элементов, то произведение по i∈s является леворарегулярным.

LaTeX

$$((∀ i ∈ s, IsLeftRegular (f i)) → IsLeftRegular (∏ i ∈ s, f i))$$

Lean4

theorem prod (h : ∀ i ∈ s, IsLeftRegular (f i)) : IsLeftRegular (∏ i ∈ s, f i) :=
  s.prod_induction _ _ (@IsLeftRegular.mul R _) isRegular_one.left h

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