English
IsDynNetIn(T, F, U, n, s) holds iff s ⊆ F and the family {ball x(dynEntourage(T,U,n)) : x ∈ s} is pairwise disjoint.
Русский
IsDynNetIn(T, F, U, n, s) верно тогда, когда s ⊆ F и семейство шаров {ball x(dynEntourage(T,U,n))} для x ∈ s пары не пересекаются.
LaTeX
$$$IsDynNetIn(T,F,U,n,s) \iff (s \subseteq F) \land (s \text{ is PairwiseDisjoint for } x \mapsto ball(x,\;dynEntourage(T,U,n))).$$$
Lean4
/-- Given a subset `F`, an entourage `U` and an integer `n`, a subset `s` of `F` is a
`(U, n)`-dynamical net of `F` if no two orbits of length `n` of points in `s` shadow each other. -/
def IsDynNetIn (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) (s : Set X) : Prop :=
s ⊆ F ∧ s.PairwiseDisjoint fun x : X ↦ ball x (dynEntourage T U n)
