coverEntropy_monotone

Mathlib.Dynamics.TopologicalEntropy.Subset

URI: https://scilib.ai/kg/mathlib#Dynamics.coverEntropy_monotone

← MathLib Explorer

English

The coverEntropy functional is monotone with respect to the input set.

Русский

Функционал coverEntropy монотонен по входному множеству.

LaTeX

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

Lean4

theorem coverEntropy_monotone [UniformSpace X] (T : X → X) : Monotone fun F : Set X ↦ coverEntropy T F := fun _ _ F_G ↦
  iSup₂_mono fun U _ ↦ coverEntropyEntourage_monotone T U F_G

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru