netMaxcard_monotone_time — Mathlib

English

For fixed T, F, U, the function n ↦ netMaxcard(T,F,U,n) is monotone: increasing n does not decrease the maximal cardinal.

Русский

Для фиксированных T, F, U функция n ↦ netMaxcard(T,F,U,n) монотонна по времени: при возрастании n максимальная кардинальность не уменьшается.

LaTeX

$$Monotone fun n: ℕ ↦ netMaxcard(T,F,U,n).$$

Lean4

theorem netMaxcard_monotone_time (T : X → X) (F : Set X) (U : Set (X × X)) : Monotone fun n : ℕ ↦ netMaxcard T F U n :=
  fun _ _ m_n ↦ biSup_mono fun _ h ↦ h.of_le m_n

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