netEntropyInfEntourage_antitone — Mathlib

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)

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