English
There exists a natural notion of grading (min-order) between Multiset α and Finset α, using the underlying Finset α inclusion, which preserves the covering relation.
Русский
Существует естественное ранжирование между Multiset α и Finset α, задаваемое вложением Finset α ↪ Multiset α, сохраняющее отношение покрытия.
LaTeX
$$$ \text{GradeMinOrder}(\operatorname{Multiset} \alpha, \operatorname{Finset} \alpha) $$$
Lean4
/-- Finsets are multiset-graded. This is not very meaningful mathematically but rather a handy way
to record that the inclusion `Finset α ↪ Multiset α` preserves the covering relation. -/
instance instGradeMinOrder_multiset : GradeMinOrder (Multiset α) (Finset α)
where
grade := val
grade_strictMono := val_strictMono
covBy_grade _ _ := CovBy.finset_val
isMin_grade s hs := by rw [isMin_iff_eq_bot.1 hs]; exact isMin_bot
