Documentation

Mathlib.Data.Finset.Grade

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 #

@[simp]
theorem Multiset.covBy_cons {α : Type u_1} (s : Multiset α) (a : α) :
s a ::ₘ s
theorem CovBy.exists_multiset_cons {α : Type u_1} {s : Multiset α} {t : Multiset α} (h : s t) :
∃ (a : α), a ::ₘ s = t
theorem Multiset.covBy_iff {α : Type u_1} {s : Multiset α} {t : Multiset α} :
s t ∃ (a : α), a ::ₘ s = t
theorem CovBy.card_multiset {α : Type u_1} {s : Multiset α} {t : Multiset α} (h : s t) :
Multiset.card s Multiset.card t
theorem Multiset.isAtom_iff {α : Type u_1} {s : Multiset α} :
IsAtom s ∃ (a : α), s = {a}
@[simp]
theorem Multiset.isAtom_singleton {α : Type u_1} (a : α) :
IsAtom {a}
Equations
@[simp]
theorem Multiset.grade_eq {α : Type u_1} (m : Multiset α) :
grade m = Multiset.card m

Finsets form an order-connected suborder of multisets.

Finsets form an order-connected suborder of sets.

@[simp]
theorem Finset.val_wcovBy_val {α : Type u_1} {s : Finset α} {t : Finset α} :
s.val ⩿ t.val s ⩿ t
@[simp]
theorem Finset.val_covBy_val {α : Type u_1} {s : Finset α} {t : Finset α} :
s.val t.val s t
@[simp]
theorem Finset.coe_wcovBy_coe {α : Type u_1} {s : Finset α} {t : Finset α} :
s ⩿ t s ⩿ t
@[simp]
theorem Finset.coe_covBy_coe {α : Type u_1} {s : Finset α} {t : Finset α} :
s t s t
theorem WCovBy.finset_val {α : Type u_1} {s : Finset α} {t : Finset α} :
s ⩿ ts.val ⩿ t.val

Alias of the reverse direction of Finset.val_wcovBy_val.

theorem CovBy.finset_val {α : Type u_1} {s : Finset α} {t : Finset α} :
s ts.val t.val

Alias of the reverse direction of Finset.val_covBy_val.

theorem WCovBy.finset_coe {α : Type u_1} {s : Finset α} {t : Finset α} :
s ⩿ ts ⩿ t

Alias of the reverse direction of Finset.coe_wcovBy_coe.

theorem CovBy.finset_coe {α : Type u_1} {s : Finset α} {t : Finset α} :
s ts t

Alias of the reverse direction of Finset.coe_covBy_coe.

@[simp]
theorem Finset.covBy_cons {α : Type u_1} {s : Finset α} {a : α} (ha : as) :
s Finset.cons a s ha
theorem CovBy.exists_finset_cons {α : Type u_1} {s : Finset α} {t : Finset α} (h : s t) :
∃ (a : α) (ha : as), Finset.cons a s ha = t
theorem Finset.covBy_iff_exists_cons {α : Type u_1} {s : Finset α} {t : Finset α} :
s t ∃ (a : α) (ha : as), Finset.cons a s ha = t
theorem CovBy.card_finset {α : Type u_1} {s : Finset α} {t : Finset α} (h : s t) :
s.card t.card
@[simp]
theorem Finset.wcovBy_insert {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
s ⩿ insert a s
@[simp]
theorem Finset.erase_wcovBy {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
theorem Finset.covBy_insert {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] (ha : as) :
s insert a s
@[simp]
theorem Finset.erase_covBy {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] (ha : a s) :
theorem CovBy.exists_finset_insert {α : Type u_1} {s : Finset α} {t : Finset α} [DecidableEq α] (h : s t) :
∃ a ∉ s, insert a s = t
theorem CovBy.exists_finset_erase {α : Type u_1} {s : Finset α} {t : Finset α} [DecidableEq α] (h : s t) :
∃ a ∈ t, Finset.erase t a = s
theorem Finset.covBy_iff_exists_insert {α : Type u_1} {s : Finset α} {t : Finset α} [DecidableEq α] :
s t ∃ a ∉ s, insert a s = t
theorem Finset.covBy_iff_card_sdiff_eq_one {α : Type u_1} {s : Finset α} {t : Finset α} [DecidableEq α] :
t s t s (s \ t).card = 1
theorem Finset.covBy_iff_exists_erase {α : Type u_1} {s : Finset α} {t : Finset α} [DecidableEq α] :
s t ∃ a ∈ t, Finset.erase t a = s
@[simp]
theorem Finset.isAtom_singleton {α : Type u_1} (a : α) :
IsAtom {a}
theorem Finset.isAtom_iff {α : Type u_1} {s : Finset α} :
IsAtom s ∃ (a : α), s = {a}
theorem Finset.isCoatom_compl_singleton {α : Type u_1} [Fintype α] [DecidableEq α] (a : α) :
theorem Finset.isCoatom_iff {α : Type u_1} {s : Finset α} [Fintype α] [DecidableEq α] :
IsCoatom s ∃ (a : α), s = {a}

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
@[simp]
theorem Finset.grade_multiset_eq {α : Type u_1} (s : Finset α) :
grade (Multiset α) s = s.val
Equations
@[simp]
theorem Finset.grade_eq {α : Type u_1} (s : Finset α) :
grade s = s.card