coverMincard_monotone_subset — Mathlib

English

The function that assigns the maximal network cardinality is monotone with respect to set inclusion.

Русский

Функция, присваивающая максимальную сетевую кардинальность, монотонна по включению множеств.

LaTeX

$$$\\text{Monotone}(\\lambda F. \\mathrm{netMaxcard}(T, F, U, n))$$$

Lean4

theorem coverMincard_monotone_subset (T : X → X) (U : Set (X × X)) (n : ℕ) :
    Monotone fun F : Set X ↦ coverMincard T F U n := fun _ _ F_G ↦ biInf_mono fun _ h ↦ h.monotone_subset F_G

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