netEntropyEntourage_nonneg — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem netEntropyEntourage_nonneg (T : X → X) {F : Set X} (h : F.Nonempty) (U : Set (X × X)) :
    0 ≤ netEntropyEntourage T F U :=
  (netEntropyInfEntourage_nonneg T h U).trans (netEntropyInfEntourage_le_netEntropyEntourage T F U)

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