coe_nonneg — Mathlib

English

Nonnegativity on Germ is equivalent to eventual nonnegativity of the representative.

Русский

Неотрицательность жермы равна неотрицательности по существованию выборки функции-образа.

LaTeX

$$$0 \le (f :\\mathrm{Germ}(l,\\beta)) \iff \\forall\\ᶠ x \\in l, 0 \le f(x)$$$

Lean4

theorem coe_nonneg [LE β] [Zero β] {f : α → β} : 0 ≤ (f : Germ l β) ↔ ∀ᶠ x in l, 0 ≤ f x :=
  Iff.rfl

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