periodic_prod — Mathlib

English

If every function in a multiset s of α → β is c-periodic, then the product s.prod is c-periodic.

Русский

Если каждая функция в мультимножестве s функций α → β имеет период c, то произведение s.prod имеет период c.

LaTeX

$$$\\forall s:\\,\\text{Multiset}(α→β), (\\forall f ∈ s, Periodic(f,c)) ⇒ Periodic(s.prod,c)$$$

Lean4

@[to_additive]
theorem _root_.Multiset.periodic_prod [Add α] [CommMonoid β] (s : Multiset (α → β)) (hs : ∀ f ∈ s, Periodic f c) :
    Periodic s.prod c :=
  (s.prod_toList ▸ s.toList.periodic_prod) fun f hf => hs f <| Multiset.mem_toList.mp hf

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