lt_iff_le_not_ge

Mathlib.Algebra.Order.Ring.Unbundled.Rat

URI: https://scilib.ai/kg/mathlib#Rat.lt_iff_le_not_ge

English

For rationals, a < b iff a ≤ b and not (b ≤ a).

Русский

Для рациональных чисел: a < b тогда и только тогда a ≤ b и не(b ≤ a).

LaTeX

$$$$a < b \\iff a \\le b \\land \\neg(b \\le a).$$$$

Lean4

protected theorem lt_iff_le_not_ge (a b : ℚ) : a < b ↔ a ≤ b ∧ ¬b ≤ a := by
  rw [← Rat.not_le, and_iff_right_of_imp Rat.le_total.resolve_left]

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

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

Разделы

Аффилиация

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