coverEntropy_iUnion_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem coverEntropy_iUnion_le (T : X → X) (F : ι → Set X) : ⨆ i, coverEntropy T (F i) ≤ coverEntropy T (⋃ i, F i) :=
  iSup_le fun i ↦ coverEntropy_monotone T (subset_iUnion F i)

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