Finsets and multisets form a graded order #
This file characterises atoms, coatoms and the covering relation in finsets and multisets. It also
proves that they form a ℕ
-graded order.
Main declarations #
Multiset.instGradeMinOrder_nat
: Multisets areℕ
-gradedFinset.instGradeMinOrder_nat
: Finsets areℕ
-graded
Equations
- Multiset.instGradeMinOrder = { grade := Multiset.card, grade_strictMono := ⋯, covBy_grade := ⋯, isMin_grade := ⋯ }
Finsets form an order-connected suborder of multisets.
Finsets form an order-connected suborder of sets.
Alias of the reverse direction of Finset.val_wcovBy_val
.
Alias of the reverse direction of Finset.val_covBy_val
.
Alias of the reverse direction of Finset.coe_wcovBy_coe
.
Alias of the reverse direction of Finset.coe_covBy_coe
.
theorem
CovBy.exists_finset_cons
{α : Type u_1}
{s t : Finset α}
(h : s ⋖ t)
:
∃ (a : α) (ha : a ∉ s), Finset.cons a s ha = t
@[simp]
@[simp]
@[simp]
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.
Equations
- Finset.instGradeMinOrder_multiset = { grade := Finset.val, grade_strictMono := ⋯, covBy_grade := ⋯, isMin_grade := ⋯ }
Equations
- Finset.instGradeMinOrder_nat = { grade := Finset.card, grade_strictMono := ⋯, covBy_grade := ⋯, isMin_grade := ⋯ }