tsub_le_tsub_iff_right

Mathlib.Algebra.Order.Sub.Unbundled.Basic

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

English

If c ≤ b, then a − c ≤ b − c iff a ≤ b.

Русский

Если c ≤ b, то a − c ≤ b − c эквивалентно a ≤ b.

LaTeX

$$$ a - c \\le b - c \\iff a \\le b $$$

Lean4

theorem tsub_le_tsub_iff_right (h : c ≤ b) : a - c ≤ b - c ↔ a ≤ b := by rw [tsub_le_iff_right, tsub_add_cancel_of_le h]

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

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

Разделы

Аффилиация

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