nonneg — Mathlib

English

Let f be a smooth partition of unity on M indexed by ι. Then for every index i and every point x in M, the value f_i(x) is nonnegative.

Русский

Пусть f — гладкое разбиение единиц на многообразии M с индексами ι. Тогда для каждого i и каждой точки x ∈ M выполняется f_i(x) ≥ 0.

LaTeX

$$$\forall i:\iota,\forall x:\,M,\ f_i(x) \ge 0$$$

Lean4

theorem nonneg (i : ι) (x : M) : 0 ≤ f i x :=
  f.nonneg' i x

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