coverEntropyInfEntourage_image_le

English

Similarly for infimum-entourage bounds: the image under φ cannot increase the infimum-entourage compared to the source with the preimage relation.

Русский

Аналогично для инфимум-entourage: образ через φ не увеличивает инфимум-entourage по сравнению с исходной связью через предобраз.

LaTeX

$$$\\operatorname{coverEntropyInfEntourage}(T, \\phi(F), V) \\le \\operatorname{coverEntropyInfEntourage}(S, F, (\\phi \\times \\phi)^{-1}(V))$$$

Lean4

theorem coverEntropyInfEntourage_image_le (h : Semiconj φ S T) (F : Set X) (V : Set (Y × Y)) :
    coverEntropyInfEntourage T (φ '' F) V ≤ coverEntropyInfEntourage S F ((map φ φ) ⁻¹' V) :=
  expGrowthInf_monotone fun n ↦ ENat.toENNReal_mono (coverMincard_image_le h F V n)

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