coverEntropyInf_le_coverEntropy — Mathlib

English

The map sending a uniformity to coverEntropyInf T F is antitone; refining the entourages decreases the entropy, i.e., if U ⊆ V then coverEntropyInfEntourage(T,F,U) ≥ coverEntropyInfEntourage(T,F,V).

Русский

Отображение униформности в coverEntropyInf T F антитонно: если окрестности менее детализированы (U ⊆ V), то энтропия по U не меньше энтропии по V.

LaTeX

$$$U \subseteq V \implies \operatorname{coverEntropyInfEntourage}(T,F,U) \ge \operatorname{coverEntropyInfEntourage}(T,F,V).$$$

Lean4

theorem coverEntropyInf_le_coverEntropy (T : X → X) (F : Set X) : coverEntropyInf T F ≤ coverEntropy T F :=
  iSup₂_mono fun (U : Set (X × X)) (_ : U ∈ 𝓤 X) ↦ coverEntropyInfEntourage_le_coverEntropyEntourage T F U

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