le_iff_lt_or_eq

Mathlib.Order.Defs.PartialOrder

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

English

For all a, b with a ≤ b, a ≤ b iff a < b or a = b (using decidability).

Русский

Для любых a, b с a ≤ b, a ≤ b эквивалентно a < b или a = b (с использованием разрешимости).

LaTeX

$$$a \le b \iff a < b ∨ a = b$$$

Lean4

theorem le_iff_lt_or_eq : a ≤ b ↔ a < b ∨ a = b :=
  open scoped Classical in Decidable.le_iff_lt_or_eq

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

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

Разделы

Аффилиация

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