sym2_mono

Mathlib.Data.Multiset.Sym

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

← MathLib Explorer

English

The map m ↦ m.sym2 is monotone with respect to inclusion.

Русский

Отображение m ↦ m.sym2 монотонно по включению.

LaTeX

$$$ \\text{Monotone}(\\mathrm{Sym2}) $$$

Lean4

@[simp, mono]
theorem sym2_mono {m m' : Multiset α} (h : m ≤ m') : m.sym2 ≤ m'.sym2 :=
  by
  refine Quotient.inductionOn₂ m m' (fun xs ys h => ?_) h
  suffices xs <+~ ys from this.sym2
  simpa only [quot_mk_to_coe, coe_le, sym2_coe] using h

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

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

Разделы

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

Аффилиация

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