English
The function n ↦ coverMincard T F U n is monotone nonincreasing in time in the formal sense, i.e., coverMincard T F U n ≤ coverMincard T F U m whenever n ≤ m.
Русский
Функция времени покрытия монотонно не возрастает по времени: coverMincard(T,F,U,n) ≤ coverMincard(T,F,U,m) при n ≤ m.
LaTeX
$$$\text{coverMincard}(T,F,U,n) \leq \text{coverMincard}(T,F,U,m)$ for $n \le m$$$
Lean4
/-- The smallest cardinality of a `(U, n)`-dynamical cover of `F`. Takes values in `ℕ∞`, and is
infinite if and only if `F` admits no finite dynamical cover. -/
noncomputable def coverMincard (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) : ℕ∞ :=
⨅ (s : Finset X) (_ : IsDynCoverOf T F U n s), (s.card : ℕ∞)