∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F : Set X} {n : ℕ} [U.IsSymm] {s : Finset X},
  Dynamics.IsDynCoverOf T F U n ↑s →
    ∃ t,
      Dynamics.IsDynCoverOf T F U n ↑t ∧
        t.card ≤ s.card ∧ ∀ x ∈ t, (UniformSpace.ball x (Dynamics.dynEntourage T U n) ∩ F).Nonempty