coverEntropy_antitone — Mathlib

English

The entropy of T restricted to F, considered as a function of the ambient uniformity, is antitone: as the entourage becomes finer, the entropy does not increase.

Русский

Энтропия T на F, рассматриваемая как функция от окружающей униформности, является антитонной: при увеличении точности окрестностей энтропия не возрастает.

LaTeX

$$$\text{Antitone }\bigl(u \mapsto \operatorname{coverEntropy}(T,F)\bigr)$, i.e. if $U \subseteq V$ then $\operatorname{coverEntropy}(T,F;U) \ge \operatorname{coverEntropy}(T,F;V)$.$$

Lean4

theorem coverEntropy_antitone (T : X → X) (F : Set X) : Antitone fun (u : UniformSpace X) ↦ @coverEntropy X u T F :=
  fun _ _ h ↦ iSup₂_mono' fun U U_uni ↦ ⟨U, (le_def.1 h) U U_uni, le_refl _⟩

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