add_eq_right_iff

Mathlib.Algebra.Tropical.Basic

URI: https://scilib.ai/kg/mathlib#Tropical.add_eq_right_iff

English

In Tropical R with a linear order, x + y = y iff y ≤ x.

Русский

В линейно упорядоченном Tropical R, x + y = y тогда, когда y ≤ x.

LaTeX

$$$x + y = y \\iff y \\le x$$$

Lean4

theorem add_eq_right_iff {x y : Tropical R} : x + y = y ↔ y ≤ x := by
  rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_right_iff]

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

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

Разделы

Аффилиация

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