iterate — Mathlib

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

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