exists_pos — Mathlib

English

Each value f_i(x) does not exceed 1: f_i(x) ≤ 1 for all i, x.

Русский

Каждое значение f_i(x) не превосходит 1: f_i(x) ≤ 1 для всех i, x.

LaTeX

$$$\forall i, \forall x,\ f_i(x) \le 1$$$

Lean4

/-- If `f` is a partition of unity on `s`, then for every `x ∈ s` there exists an index `i` such
that `0 < f i x`. -/
theorem exists_pos {x : X} (hx : x ∈ s) : ∃ i, 0 < f i x :=
  by
  have H := f.sum_eq_one hx
  contrapose! H
  simpa only [fun i => (H i).antisymm (f.nonneg i x), finsum_zero] using zero_ne_one

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