netEntropyEntourage_monotone — Mathlib

English

The coverEntropyEntourage functional is monotone with respect to its input set.

Русский

Функционал coverEntropyEntourage монотонен по входному множеству.

LaTeX

$$$\\text{Monotone}(F \\mapsto \\mathrm{coverEntropyEntourage}(T, F, U))$$$

Lean4

theorem netEntropyEntourage_monotone (T : X → X) (U : Set (X × X)) :
    Monotone fun F : Set X ↦ netEntropyEntourage T F U :=
  by
  refine fun F G F_G ↦ ExpGrowth.expGrowthSup_monotone fun n ↦ ?_
  exact ENat.toENNReal_mono (netMaxcard_monotone_subset T U n F_G)

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