coverEntropyInfEntourage_univ — Mathlib

English

For any nonempty F, coverEntropyInfEntourage T F univ = 0.

Русский

Для любого непустого F coverEntropyInfEntourage T F univ = 0.

LaTeX

$$$coverEntropyInfEntourage(T,F,\univ)=0$$$

Lean4

theorem coverEntropyInfEntourage_univ (T : X → X) {F : Set X} (h : F.Nonempty) :
    coverEntropyInfEntourage T F univ = 0 :=
  by
  rw [← expGrowthInf_const one_ne_zero one_ne_top, coverEntropyInfEntourage]
  simp only [coverMincard_univ T h, ENat.toENNReal_one]

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