prod — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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