coverMincard_monotone_time — Mathlib

English

The map n ↦ coverMincard T F U n is monotone decreasing with respect to n when interpreted in ENat.

Русский

Покрытие минимальной мощности монотонно убывает по времени n при использовании ENat.

LaTeX

$$Monotone fun n => coverMincard T F U n$$

Lean4

theorem coverMincard_monotone_time (T : X → X) (F : Set X) (U : Set (X × X)) :
    Monotone fun n : ℕ ↦ coverMincard T F U n := fun _ _ m_n ↦ biInf_mono fun _ h ↦ h.of_le m_n

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