netMaxcard_monotone_subset

Mathlib.Dynamics.TopologicalEntropy.Subset

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

← MathLib Explorer

English

The net entropy over sets is monotone with respect to inclusion.

Русский

Сеточная энтропия монотонна по включению множеств.

LaTeX

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

Lean4

theorem netMaxcard_monotone_subset (T : X → X) (U : Set (X × X)) (n : ℕ) :
    Monotone fun F : Set X ↦ netMaxcard T F U n := fun _ _ F_G ↦ biSup_mono fun _ h ↦ h.monotone_subset F_G

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

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

Разделы

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

Аффилиация

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