coverEntropyEntourage_monotone — Mathlib

English

A parallel monotonicity result for coverEntropyEntourage holds for all X, with S, T and φ in the semiconjugacy relation.

Русский

Похожее свойство монотонности для coverEntropyEntourage справедливо во всей системе X при наличии семиконъюгатной связи между S, T и φ.

LaTeX

$$$\\text{Monotone}(F \\mapsto \\mathrm{coverEntropyEntourage}(T, F, U))$$$

Lean4

theorem coverEntropyEntourage_monotone (T : X → X) (U : Set (X × X)) :
    Monotone fun F : Set X ↦ coverEntropyEntourage T F U :=
  by
  refine fun F G F_G ↦ ExpGrowth.expGrowthSup_monotone fun n ↦ ?_
  exact ENat.toENNReal_mono (coverMincard_monotone_subset T U n F_G)

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