English
A subset s of X is a (U, n)-dynamical cover of F if every point of F is U-shadowed by an n-step orbit starting in s; equivalently F is contained in the union over x in s of ball x (dynEntourage(T, U, n)).
Русский
Подмножество s ⊆ X называется (U, n)-динамическим покрытием F, если каждая точка из F лежит в тени орбиты длиной n, исходящей из некоторой точки из s; то есть F ⊆ ⋃_{x∈s} B(x, dynEntourage(T,U,n)).
LaTeX
$$$F \subseteq \bigcup_{x \in s} \mathrm{ball}\,x\big(\mathrm{dynEntourage}(T, U, n)\big)$$$
Lean4
/-- Given a subset `F`, an entourage `U` and an integer `n`, a subset `s` is a `(U, n)`-
dynamical cover of `F` if any orbit of length `n` in `F` is `U`-shadowed by an orbit of length `n`
of a point in `s`. -/
def IsDynCoverOf (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) (s : Set X) : Prop :=
F ⊆ ⋃ x ∈ s, ball x (dynEntourage T U n)
