coverEntropyInf_biUnion_le — Mathlib

English

For any s ⊆ ι, the supremum of coverEntropyInf over i ∈ s is bounded by the entropy over the biunion: ⨆ i ∈ s, coverEntropyInf T (F i) ≤ coverEntropyInf T (⋃ i ∈ s, F i).

Русский

Для подмножеств индексов s эффективный верхний предел энтропии инф по i ∈ s не больше энтропии объединения по i ∈ s.

LaTeX

$$$\sup_{i \in s} \operatorname{coverEntropyInf}(T, F_i) \le \operatorname{coverEntropyInf}(T, \bigcup_{i \in s} F_i)$$$

Lean4

theorem coverEntropyInf_biUnion_le (s : Set ι) (T : X → X) (F : ι → Set X) :
    ⨆ i ∈ s, coverEntropyInf T (F i) ≤ coverEntropyInf T (⋃ i ∈ s, F i) :=
  iSup₂_le fun _ i_s ↦ coverEntropyInf_monotone T (subset_biUnion_of_mem i_s)

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