single_nonneg — Mathlib

English

Let α be a ordered additive structure with a zero. For any i in ι and a in α, the singleton function δ_i(a) is nonnegative iff a is nonnegative: 0 ≤ single i a ⇔ 0 ≤ a.

Русский

Пусть α — упорядоченная добавочная структура с нулём. Для любого i ∈ ι и a ∈ α выполнено: δ_i(a) ≥ 0 тогда и только тогда, когда a ≥ 0.

LaTeX

$$$0 \le \mathrm{single}(i,a)$$$

Lean4

@[simp]
theorem single_nonneg : 0 ≤ single i a ↔ 0 ≤ a := by classical exact Pi.single_nonneg

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