le_iff

Mathlib.Data.Finsupp.Order

URI: https://scilib.ai/kg/mathlib#Finsupp.le_iff

English

For finsupp f,g, f ≤ g if and only if f(i) ≤ g(i) for all i in supp(f).

Русский

Для функций с конечной опорой f,g: f ≤ g тогда и только тогда, когда f(i) ≤ g(i) для всех i в supp(f).

LaTeX

$$f ≤ g \iff \forall i ∈ \mathrm{supp}(f), f(i) ≤ g(i)$$

Lean4

theorem le_iff (f g : ι →₀ α) : f ≤ g ↔ ∀ i ∈ f.support, f i ≤ g i :=
  le_iff' f g <| Subset.refl _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru