netEntropyEntourage_le_coverEntropyEntourage

English

For a symmetric U, netEntropyEntourage T F U ≤ coverEntropyEntourage T F U.

Русский

Для симметричной U: netEntropyEntourage T F U ≤ coverEntropyEntourage T F U.

LaTeX

$$$\text{netEntropyEntourage}(T,F,U)\le \text{coverEntropyEntourage}(T,F,U)$$$

Lean4

theorem netEntropyEntourage_le_coverEntropyEntourage (T : X → X) (F : Set X) {U : Set (X × X)}
    (U_symm : IsSymmetricRel U) : netEntropyEntourage T F U ≤ coverEntropyEntourage T F U :=
  expGrowthSup_monotone fun n ↦ ENat.toENNReal_mono (netMaxcard_le_coverMincard T F U_symm n)

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