coverEntropyEntourage_antitone — Mathlib

English

The entropy of an entourage decreases when the entourage becomes larger, i.e., U ⊆ V implies coverEntropyEntourage(T,F,V) ≤ coverEntropyEntourage(T,F,U).

Русский

Энтропия окружения уменьшается при увеличении окружения: U ⊆ V → coverEntropyEntourage(T,F,V) ≤ coverEntropyEntourage(T,F,U).

LaTeX

$$Antitone\, (U,V)\; (U \subseteq V) \\Rightarrow\; coverEntropyEntourage(T,F,V) \le coverEntropyEntourage(T,F,U)$$

Lean4

theorem coverEntropyEntourage_antitone (T : X → X) (F : Set X) :
    Antitone fun U : Set (X × X) ↦ coverEntropyEntourage T F U := fun _ _ U_V ↦
  expGrowthSup_monotone fun n ↦ ENat.toENNReal_mono (coverMincard_antitone T F n U_V)

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