netEntropyInfEntourage_nonneg — Mathlib

English

If F is nonempty, then netEntropyInfEntourage T F U ≥ 0, i.e., 0 ≤ netEntropyInfEntourage T F U.

Русский

Если F непусто, то netEntropyInfEntourage T F U неотрицательно.

LaTeX

$$$F\neq\emptyset\Rightarrow 0\le \operatorname{netEntropyInfEntourage}(T,F,U)$$$

Lean4

theorem netEntropyInfEntourage_nonneg (T : X → X) {F : Set X} (h : F.Nonempty) (U : Set (X × X)) :
    0 ≤ netEntropyInfEntourage T F U := by
  apply Monotone.expGrowthInf_nonneg
  · exact fun _ _ m_n ↦ ENat.toENNReal_mono (netMaxcard_monotone_time T F U m_n)
  · rw [ne_eq, funext_iff.not, not_forall]
    use 0
    rw [netMaxcard_zero T h U, Pi.zero_apply, ENat.toENNReal_one]
    exact one_ne_zero

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