coverMincard_le_card — Mathlib

English

If IsDynCoverOf T F U n s holds, then coverMincard T F U n is bounded above by s.card, i.e., coverMincard ≤ s.card.

Русский

Если покрытие существует, то минимальная-cardinality не превышает число элементов в s.

LaTeX

$$coverMincard T F U n ≤ |s|$$

Lean4

theorem coverMincard_le_card {T : X → X} {F : Set X} {U : Set (X × X)} {n : ℕ} {s : Finset X}
    (h : IsDynCoverOf T F U n s) : coverMincard T F U n ≤ s.card :=
  iInf₂_le s h

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