English
A point y lies in the ball around x with radius dynEntourage(T,U,n) if and only if for all k < n, T^k y lies in the ball around T^k x with respect to U.
Русский
Точка y принадлежит шар вокруг x радиуса dynEntourage(T,U,n) тогда и только тогда, когда для всех k < n T^k y лежит в шаре вокруг T^k x по U.
LaTeX
$$$y \in \mathrm{ball}(x, \mathrm{dynEntourage}(T,U,n)) \iff \forall k < n, T^{k}y \in \mathrm{ball}(T^{k}x, U)$$$
Lean4
theorem mem_ball_dynEntourage {T : X → X} {U : Set (X × X)} {n : ℕ} {x y : X} :
y ∈ ball x (dynEntourage T U n) ↔ ∀ k < n, T^[k] y ∈ ball (T^[k] x) U := by
simp only [ball, mem_preimage, mem_dynEntourage]