netEntropyInfEntourage_monotone — Mathlib

English

The net entropy entourage functional is monotone with respect to set inclusion.

Русский

Функционал сетевой энтропии-окружения монотонен по включению множеств.

LaTeX

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

Lean4

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

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