coverEntropyInf_empty — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem coverEntropyInf_empty {T : X → X} : coverEntropyInf T ∅ = ⊥ := by
  simp only [coverEntropyInf, coverEntropyInfEntourage_empty, iSup_bot]

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