toMultiset_lt_toMultiset

Mathlib.Data.DFinsupp.Multiset

URI: https://scilib.ai/kg/mathlib#DFinsupp.toMultiset_lt_toMultiset

← MathLib Explorer

English

toMultiset preserves the strict order: f < g iff toMultiset f < toMultiset g.

Русский

toMultiset сохраняет строгий порядок: f < g эквивалентно toMultiset f < toMultiset g.

LaTeX

$$$$ \\operatorname{toMultiset} f < \\operatorname{toMultiset} g \\iff f < g $$$$

Lean4

@[simp]
theorem toMultiset_lt_toMultiset : toMultiset f < toMultiset g ↔ f < g := by
  simp_rw [← Multiset.toDFinsupp_lt_toDFinsupp, toMultiset_toDFinsupp]

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

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

Разделы

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

Аффилиация

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