coverEntropyEntourage_nonneg — Mathlib

English

For any nonempty F and U, the entropy of the entourage is nonnegative: 0 ≤ coverEntropyEntourage T F U.

Русский

Для любого непустого F и U энтропия окружения неотрицательна.

LaTeX

$$0 \leq coverEntropyEntourage(T,F,U)$$

Lean4

theorem coverEntropyEntourage_nonneg (T : X → X) {F : Set X} (h : F.Nonempty) (U : Set (X × X)) :
    0 ≤ coverEntropyEntourage T F U :=
  (coverEntropyInfEntourage_nonneg T h U).trans (coverEntropyInfEntourage_le_coverEntropyEntourage T F U)

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