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)