coverEntropyInf_iUnion_le — Mathlib

English

For any T and a family F: ι → Set X, the supremum of coverEntropyInf over i is bounded by the entropy of the union: ⨆ i, coverEntropyInf T (F i) ≤ coverEntropyInf T (⋃ i, F i).

Русский

Для семейства F: ι →Set X верхняя граница по i для coverEntropyInf меньше или равна entropии объединения.

LaTeX

$$$\sup_i \operatorname{coverEntropyInf}(T, F_i) \le \operatorname{coverEntropyInf}(T, \bigcup_i F_i)$$$

Lean4

theorem coverEntropyInf_iUnion_le (T : X → X) (F : ι → Set X) :
    ⨆ i, coverEntropyInf T (F i) ≤ coverEntropyInf T (⋃ i, F i) :=
  iSup_le fun i ↦ coverEntropyInf_monotone T (subset_iUnion F i)

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