cons_le_cons

Mathlib.Data.Multiset.ZeroCons

URI: https://scilib.ai/kg/mathlib#Multiset.cons_le_cons

English

If s ≤ t, then inserting a into both sides preserves the inequality.

Русский

Если s ≤ t, то вставка a в оба множества сохранит неравенство.

LaTeX

$$$s \le t \Rightarrow insert(a, s) \le insert(a, t)$$$

Lean4

theorem cons_le_cons (a : α) : s ≤ t → a ::ₘ s ≤ a ::ₘ t :=
  (cons_le_cons_iff a).2

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

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

Разделы

Аффилиация

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