fromIter — Mathlib

English

Iterations of a continuous map g: α → α define a semiflow by ℕ on α.

Русский

Повторения непрерывной карты g: α → α задают полупоток по ℕ на α.

LaTeX

$$$\text{fromIter}(g) : \text{Flow } \mathbb{N} \alpha \quad\text{with } (n, x) \mapsto g^{[n]}(x)$$$

Lean4

/-- Iterations of a continuous function from a topological space `α`
to itself defines a semiflow by `ℕ` on `α`. -/
def fromIter {g : α → α} (h : Continuous g) : Flow ℕ α
    where
  toFun n x := g^[n] x
  cont' := continuous_prod_of_discrete_left.mpr (Continuous.iterate h)
  map_add' := iterate_add_apply _
  map_zero' _x := rfl

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