dynEntourage — Mathlib

English

The dynamical entourage dynEntourage(T,U,n) is the set of pairs (x,y) such that (T^k x, T^k y) ∈ U for all k < n.

Русский

Динамическое окружение dynEntourage(T,U,n) — это множество пар (x,y), для которых (T^k x, T^k y) ∈ U для всех k < n.

LaTeX

$$$\operatorname{dynEntourage}(T,U,n) = \bigcap_{k < n} (\,(\operatorname{map} T T)^{[k]}\,)^{-1}(U)$$$

Lean4

/-- The dynamical entourage associated to a transformation `T`, entourage `U` and time `n`
is the set of points `(x, y)` such that `(T^[k] x, T^[k] y) ∈ U` for all `k < n`, i.e.
which are `U`-close up to time `n`. -/
def dynEntourage (T : X → X) (U : Set (X × X)) (n : ℕ) : Set (X × X) :=
  ⋂ k < n, (map T T)^[k] ⁻¹' U

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