instAddLeftReflectLE

Mathlib.Data.DFinsupp.Order

URI: https://scilib.ai/kg/mathlib#DFinsupp.instAddLeftReflectLE

← MathLib Explorer

English

The left addition is order-reflecting: if a + x ≤ b + x then a ≤ b.

Русский

Левая сумма задаёт отражение порядка: если a + x ≤ b + x, то a ≤ b.

LaTeX

$$$$ a + x \le b + x \Rightarrow a \le b. $$$$

Lean4

instance [∀ i, AddCommMonoid (α i)] [∀ i, PartialOrder (α i)] [∀ i, AddLeftReflectLE (α i)] :
    AddLeftReflectLE (Π₀ i, α i) :=
  ⟨fun _ _ _ H i ↦ le_of_add_le_add_left (H i)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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