netEntropyInfEntourage_le_netEntropyEntourage

English

The map U ↦ netEntropyInfEntourage(T,F,U) is antitone: refinement of U cannot increase entropy.

Русский

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

LaTeX

$$$\forall U,V\; U\subseteq V\Rightarrow \operatorname{netEntropyInfEntourage}(T,F,V)\le \operatorname{netEntropyInfEntourage}(T,F,U)$$$

Lean4

theorem netEntropyInfEntourage_le_netEntropyEntourage (T : X → X) (F : Set X) (U : Set (X × X)) :
    netEntropyInfEntourage T F U ≤ netEntropyEntourage T F U :=
  expGrowthInf_le_expGrowthSup

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