comp — Mathlib

English

If f is periodic with period c, then for any g: β → γ, the composition g ∘ f is periodic with period c.

Русский

Если f периодична с периодом c, то композиция g ∘ f периодична с тем же периодом c.

LaTeX

$$$\forall f:\alpha\to\beta,\, c,\, \mathrm{Periodic}(f,c) \Rightarrow \forall g:\beta\to\gamma,\ \mathrm{Periodic}(g \circ f, c).$$$

Lean4

protected theorem comp [Add α] (h : Periodic f c) (g : β → γ) : Periodic (g ∘ f) c := by simp_all

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