netEntropyInfEntourage_le_coverEntropyInf

English

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

Русский

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

LaTeX

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

Lean4

theorem netEntropyInfEntourage_le_coverEntropyInf {U : Set (X × X)} (h : U ∈ 𝓤 X) :
    netEntropyInfEntourage T F U ≤ coverEntropyInf T F :=
  coverEntropyInf_eq_iSup_netEntropyInfEntourage T F ▸
    le_iSup₂ (f := fun (U : Set (X × X)) (_ : U ∈ 𝓤 X) ↦ netEntropyInfEntourage T F U) U h

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