coverEntropyInf_monotone — Mathlib

English

The monotonicity of coverEntropyEntourage with respect to the set argument is established.

Русский

Установлена монотонность coverEntropyEntourage по множеству-аргументу.

LaTeX

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

Lean4

theorem coverEntropyInf_monotone [UniformSpace X] (T : X → X) : Monotone fun F : Set X ↦ coverEntropyInf T F :=
  fun _ _ F_G ↦ iSup₂_mono fun U _ ↦ coverEntropyInfEntourage_monotone T U F_G

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