netEntropyInfEntourage_le_coverEntropyInfEntourage

English

For any T, F and symmetric U, netEntropyInfEntourage T F U ≤ coverEntropyInfEntourage T F U.

Русский

Для любой T, F и симметричной U: netEntropyInfEntourage T F U ≤ coverEntropyInfEntourages T F U.

LaTeX

$$$\text{netEntropyInfEntourage}(T,F,U)\le\text{coverEntropyInfEntourage}(T,F,U)$$$

Lean4

theorem netEntropyInfEntourage_le_coverEntropyInfEntourage (T : X → X) (F : Set X) {U : Set (X × X)}
    (U_symm : IsSymmetricRel U) : netEntropyInfEntourage T F U ≤ coverEntropyInfEntourage T F U :=
  expGrowthInf_monotone fun n ↦ ENat.toENNReal_mono (netMaxcard_le_coverMincard T F U_symm n)

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