netMaxcard — Mathlib

English

netMaxcard T F U n equals ⊤ if and only if, for every k ∈ ℕ, there exists a Finset s with IsDynNetIn T F U n s and k ≤ |s|.

Русский

netMaxcard T F U n равно ⊤ тогда, когда для каждого k существует конечное множество s, удовлетворяющее IsDynNetIn и k ≤ |s|.

LaTeX

$$netMaxcard(T,F,U,n) = ⊤ \iff ∀ k ∈ ℕ, ∃ s : Finset X, IsDynNetIn(T,F,U,n,s) ∧ k ≤ s.card.$$

Lean4

/-- The largest cardinality of a `(U, n)`-dynamical net of `F`. Takes values in `ℕ∞`, and is
infinite if and only if `F` admits nets of arbitrarily large size. -/
noncomputable def netMaxcard (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) : ℕ∞ :=
  ⨆ (s : Finset X) (_ : IsDynNetIn T F U n s), (s.card : ℕ∞)

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