max_eq_left_iff

Mathlib.Order.MinMax

URI: https://scilib.ai/kg/mathlib#max_eq_left_iff

English

In a linear order, max(a,b) = a if and only if b ≤ a.

Русский

В линейном порядке max(a,b) = a тогда и только тогда, когда b ≤ a.

LaTeX

$$$$\max(a,b) = a \iff b \le a.$$$$

Lean4

theorem max_eq_left_iff : max a b = a ↔ b ≤ a :=
  sup_eq_left

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

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

Разделы

Аффилиация

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