tsub_pos_iff_not_le

Mathlib.Algebra.Order.Sub.Basic

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

English

0 < a − b iff not (a ≤ b).

Русский

0 < a − b тогда и только тогда, когда не выполняется a ≤ b.

LaTeX

$$$$ 0 < a - b \iff \neg(a \le b) $$$$

Lean4

theorem tsub_pos_iff_not_le : 0 < a - b ↔ ¬a ≤ b := by rw [pos_iff_ne_zero, Ne, tsub_eq_zero_iff_le]

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

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

Разделы

Аффилиация

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