coverEntropy_supBotHom — Mathlib

English

There exists a SupBotHom structure on coverEntropy with mapping to the real extended line, capturing monotone set relations via entropy.

Русский

Существует структура SupBotHom на coverEntropy, отображающая множество в зависимостях энтропии и сохраняющая монотонность.

LaTeX

$$$\\text{coverEntropy\_supBotHom }(T) :\\ SupBotHom (Set X) \\mathbb{R}_{\\ge -\\infty} $ with $\\text{toFun} = \\text{coverEntropy}(T)$, etc.$$

Lean4

/-- Topological entropy `CoverEntropy T` as a `SupBotHom` function of the subset. -/
noncomputable def coverEntropy_supBotHom (T : X → X) : SupBotHom (Set X) EReal
    where
  toFun := coverEntropy T
  map_sup' := fun _ _ ↦ coverEntropy_union
  map_bot' := coverEntropy_empty

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