English
If f: α → α is continuous on s and maps s into s, then every iterate f^[n] is continuous on s for all natural n.
Русский
Если f: α → α непрерывна на s и отображает s в s, то каждый повторный шаг f^[n] непрерывен на s для всех натуральных n.
LaTeX
$$$$\text{ContinuousOn } f\ s \land \text{MapsTo } f\ s\ s \Rightarrow \forall n\in\mathbb{N},\ \text{ContinuousOn } (f^{[n]})\ s.$$$$
Lean4
protected theorem iterate {f : α → α} {s : Set α} (hcont : ContinuousOn f s) (hmaps : MapsTo f s s) :
∀ n, ContinuousOn (f^[n]) s
| 0 => continuousOn_id
| (n + 1) => (hcont.iterate hmaps n).comp hcont hmaps