netEntropyEntourage_le_coverEntropy

English

If F is nonempty, netEntropyEntourage T F univ = 0.

Русский

Если F непусто, то netEntropyEntourage T F univ = 0.

LaTeX

$$$F\neq\emptyset\Rightarrow \operatorname{netEntropyEntourage}(T,F,\mathrm{univ})=0$$$

Lean4

theorem netEntropyEntourage_le_coverEntropy {U : Set (X × X)} (h : U ∈ 𝓤 X) :
    netEntropyEntourage T F U ≤ coverEntropy T F :=
  coverEntropy_eq_iSup_netEntropyEntourage T F ▸
    le_iSup₂ (f := fun (U : Set (X × X)) (_ : U ∈ 𝓤 X) ↦ netEntropyEntourage T F U) U h

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