cons_lt_cons

Mathlib.Data.Multiset.ZeroCons

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

English

If s < t, then inserting a into both sides yields a strict inequality.

Русский

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

LaTeX

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

Lean4

theorem cons_lt_cons (a : α) (h : s < t) : a ::ₘ s < a ::ₘ t :=
  cons_lt_cons_iff.2 h

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

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

Разделы

Аффилиация

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