netEntropyEntourage_antitone — Mathlib

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)

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