sub_le_iff_le_add'

Mathlib.Data.Multiset.AddSub

URI: https://scilib.ai/kg/mathlib#Multiset.sub_le_iff_le_add'

← MathLib Explorer

English

s - t ≤ u ↔ s ≤ t + u

Русский

s - t ≤ u эквивалентно s ≤ t + u.

LaTeX

$$$s - t \le u \iff s \le t + u$$$

Lean4

/-- This is a special case of `tsub_le_iff_left`, which should be used instead of this. -/
protected theorem sub_le_iff_le_add' : s - t ≤ u ↔ s ≤ t + u := by rw [Multiset.sub_le_iff_le_add, Multiset.add_comm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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