add_eq_left_iff

Mathlib.Algebra.Tropical.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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