coverMincard — Mathlib

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 : ℕ∞)

Похожие утверждения