toDFinsupp_le_toDFinsupp

Mathlib.Data.DFinsupp.Multiset

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

English

For any s,t, toDFinsupp s ≤ toDFinsupp t iff s ≤ t.

Русский

Для любых s, t: toDFinsupp s ≤ toDFinsupp t эквивалентно s ≤ t.

LaTeX

$$$$ \\operatorname{toDFinsupp} s \\le \\operatorname{toDFinsupp} t \\iff s \\le t $$$$

Lean4

@[simp]
theorem toDFinsupp_le_toDFinsupp : toDFinsupp s ≤ toDFinsupp t ↔ s ≤ t := by
  simp [Multiset.le_iff_count, DFinsupp.le_def]

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

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

Разделы

Аффилиация

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