coverEntropy_union — Mathlib

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

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