coverEntropyInfEntourage_antitone

English

The map U ↦ coverEntropyInfEntourage(T,F,U) is antitone: larger entourages (inclusion) do not increase the entropy.

Русский

Отображение U ↦ coverEntropyInfEntourage(T,F,U) антимонотно: большее окружение (по включению) не увеличивает энтропию.

LaTeX

$$Antitone\, (U,V)\; (U \subseteq V) \\Rightarrow\; coverEntropyInfEntourage(T,F,V) \le coverEntropyInfEntourage(T,F,U)$$

Lean4

theorem coverEntropyInfEntourage_antitone (T : X → X) (F : Set X) :
    Antitone fun U : Set (X × X) ↦ coverEntropyInfEntourage T F U := fun _ _ U_V ↦
  expGrowthInf_monotone fun n ↦ ENat.toENNReal_mono (coverMincard_antitone T F n U_V)

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