coverEntropy_empty

Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

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

English

The entropy over the empty set is the bottom element, i.e., coverEntropy T ∅ = ⊥.

Русский

Энтропия над пустым множеством равна нижнему элементу: coverEntropy T ∅ = ⊥.

LaTeX

$$$\operatorname{coverEntropy}(T, \emptyset) = \perp$$$

Lean4

@[simp]
theorem coverEntropy_empty {T : X → X} : coverEntropy T ∅ = ⊥ := by
  simp only [coverEntropy, coverEntropyEntourage_empty, iSup_bot]

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

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

Разделы

Аффилиация

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