netEntropyInfEntourage_empty

Mathlib.Dynamics.TopologicalEntropy.NetEntropy

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

← MathLib Explorer

English

For any T and U, netEntropyInfEntourage T ∅ U = ⊥.

Русский

Для любых T и окрестности U инфэнтропия пустой пары равна ⊥.

LaTeX

$$$\operatorname{netEntropyInfEntourage}(T,\emptyset,U)=\bot$$$

Lean4

@[simp]
theorem netEntropyInfEntourage_empty {T : X → X} {U : Set (X × X)} : netEntropyInfEntourage T ∅ U = ⊥ :=
  eq_bot_mono (netEntropyInfEntourage_le_netEntropyEntourage T ∅ U) netEntropyEntourage_empty

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

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

Разделы

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

Аффилиация

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