toMultiset_le_toMultiset — Mathlib

English

toMultiset preserves the order relation: f ≤ g iff toMultiset f ≤ toMultiset g.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toMultiset_le_toMultiset : toMultiset f ≤ toMultiset g ↔ f ≤ g := by
  simp_rw [← Multiset.toDFinsupp_le_toDFinsupp, toMultiset_toDFinsupp]

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