coverEntropyEntourage_le_coverEntropy

English

For any T and F and any entourage U, the entropy contributed by U does not exceed the total entropy: coverEntropyEntourage(T,F,U) ≤ coverEntropy(T,F).

Русский

Для любого T и F и любой окрестности U справедливо: энтропия по U не превосходит общую энтропию: coverEntropyEntourage(T,F,U) ≤ coverEntropy(T,F).

LaTeX

$$$\forall U \in \mathcal{U}(X): \operatorname{coverEntropyEntourage}(T,F,U) \le \operatorname{coverEntropy}(T,F)$$$

Lean4

theorem coverEntropyEntourage_le_coverEntropy (T : X → X) (F : Set X) {U : Set (X × X)} (h : U ∈ 𝓤 X) :
    coverEntropyEntourage T F U ≤ coverEntropy T F :=
  le_iSup₂ (f := fun (U : Set (X × X)) (_ : U ∈ 𝓤 X) ↦ coverEntropyEntourage T F U) U h

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