le_imp_eq_iff_le_imp_ge'

Mathlib.Order.Basic

URI: https://scilib.ai/kg/mathlib#le_imp_eq_iff_le_imp_ge'

English

The implication a ≤ b → b = a is equivalent to a ≤ b → b ≤ a.

Русский

Утверждение a ≤ b → b = a эквивалентно a ≤ b → b ≤ a.

LaTeX

$$$ (a \le b \to b = a) \iff (a \le b \to b \le a) $$$

Lean4

theorem le_imp_eq_iff_le_imp_ge' : (a ≤ b → b = a) ↔ (a ≤ b → b ≤ a)
    where
  mp h hab := (h hab).le
  mpr h hab := (h hab).antisymm hab

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

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

Разделы

Аффилиация

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