English
For any T, F, G, the entropy of the union equals the maximum of the entropies: coverEntropy(T, F ∪ G) = max( coverEntropy(T, F), coverEntropy(T, G) ).
Русский
Энтропия объединения равна максимуму энтропий по частям.
LaTeX
$$$\operatorname{coverEntropy}(T, F \cup G) = \max\big( \operatorname{coverEntropy}(T, F), \operatorname{coverEntropy}(T, G) \big)$$$
Lean4
theorem coverEntropy_union {T : X → X} {F G : Set X} :
coverEntropy T (F ∪ G) = max (coverEntropy T F) (coverEntropy T G) :=
by
simp only [coverEntropy, ← iSup_sup_eq]
exact biSup_congr fun _ _ ↦ coverEntropyEntourage_union