coverEntropy_iUnion_of_finite — Mathlib

English

For finite index set ι, the entropy of the union equals the supremum of the entropies: coverEntropy T (⋃ i, F i) = sup_i coverEntropy T (F i).

Русский

Для конечного множества индексов ι энтропия объединения равна верхней границе энтропий каждого множества: coverEntropy T (⋃ i, F i) = sup_i coverEntropy T (F i).

LaTeX

$$$\\operatorname{coverEntropy} T\\left(\\bigcup_{i\\in ι} F_i\\right) = \\sup_{i\\in ι} \\operatorname{coverEntropy} T(F_i)$$$

Lean4

theorem coverEntropy_iUnion_of_finite [Finite ι] {T : X → X} {F : ι → Set X} :
    coverEntropy T (⋃ i : ι, F i) = ⨆ i : ι, coverEntropy T (F i) :=
  map_finite_iSup (coverEntropy_supBotHom T) F

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