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