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