card_le_netMaxcard — Mathlib

English

netMaxcard T F U n < ∞ if and only if there exists a finite s with IsDynNetIn T F U n s and card(s) = netMaxcard T F U n.

Русский

netMaxcard T F U n < ∞ тогда и только тогда, когда существует конечное s с IsDynNetIn T F U n s и |s| = netMaxcard T F U n.

LaTeX

$$$netMaxcard(T,F,U,n) < \infty \iff ∃ s : Finset X, IsDynNetIn(T,F,U,n,s) \land (s.card : \mathbb{N}^\infty) = netMaxcard(T,F,U,n).$$$

Lean4

theorem card_le_netMaxcard {T : X → X} {F : Set X} {U : Set (X × X)} {n : ℕ} {s : Finset X} (h : IsDynNetIn T F U n s) :
    s.card ≤ netMaxcard T F U n :=
  le_iSup₂ (α := ℕ∞) s h

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