mem_dynEntourage — Mathlib

English

An (x,y) belongs to the dynamical entourage up to time n if and only if for every k with 0 ≤ k < n, (T^k x, T^k y) ∈ U.

Русский

Пара (x,y) принадлежит динамическому окружению до времени n тогда и только тогда, когда для каждого k с 0 ≤ k < n выполняется (T^k x, T^k y) ∈ U.

LaTeX

$$$(x,y) \in \operatorname{dynEntourage}(T,U,n) \iff \forall k < n, (T^{k}x, T^{k}y) \in U$$$

Lean4

theorem mem_dynEntourage {T : X → X} {U : Set (X × X)} {n : ℕ} {x y : X} :
    (x, y) ∈ dynEntourage T U n ↔ ∀ k < n, (T^[k] x, T^[k] y) ∈ U := by simp [dynEntourage]

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