English
The map U ↦ netEntropyInfEntourage(T,F,U) is antitone: if U ⊆ V then netEntropyInfEntourage(T,F,V) ≤ netEntropyInfEntourage(T,F,U).
Русский
Отображение U ↦ netEntropyInfEntourage(T,F,U) антимонотонно: если U ⊆ V, то netEntropyInfEntourage(T,F,V) ≤ netEntropyInfEntourage(T,F,U).
LaTeX
$$$\forall U,V,\; U\subseteq V\Rightarrow \operatorname{netEntropyInfEntourage}(T,F,V)\le \operatorname{netEntropyInfEntourage}(T,F,U)$$$
Lean4
theorem netEntropyInfEntourage_antitone (T : X → X) (F : Set X) :
Antitone fun U : Set (X × X) ↦ netEntropyInfEntourage T F U := fun _ _ U_V ↦
expGrowthInf_monotone fun n ↦ ENat.toENNReal_mono (netMaxcard_antitone T F n U_V)