English
Let f be a finitely supported function f: ι →₀ α, where α is an AddCommMonoid with a PartialOrder and CanonicallyOrderedAdd. Then the function that is zero everywhere except at i with value x, denoted single i x, satisfies single i x ≤ f if and only if x ≤ f(i).
Русский
Пусть f : ι →₀ α — конечно поддерживаемая функция, где α — коммутативный моноид с частичным порядком и канонически упорядоченной добавляющей структурой. Тогда единичная функция, равная x в позиции i и нулю в остальных, удовлетворяет неравенству single i x ≤ f тогда и только тогда, когда x ≤ f(i).
LaTeX
$$$\\mathrm{single}(i, x) \\le f \\iff x \\le f(i)$$$
Lean4
@[simp]
theorem single_le_iff {i : ι} {x : α} {f : ι →₀ α} : single i x ≤ f ↔ x ≤ f i :=
(le_iff' _ _ support_single_subset).trans <| by simp
