coverEntropy_biUnion_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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