le_max_left

Mathlib.Order.Defs.LinearOrder

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

English

¬(a < b) ⇔ b ≤ a.

Русский

¬(a < b) эквивалентно b ≤ a.

LaTeX

$$$ \neg(a < b) \\leftrightarrow b \le a $$$

Lean4

theorem le_max_left (a b : α) : a ≤ max a b := by
  if h : a ≤ b then simpa [max_def, if_pos h] using h else simp [max_def, if_neg h, le_refl]

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

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

Разделы

Аффилиация

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