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 ℕ-graded
• Finset.instGradeMinOrder_nat: Finsets are ℕ-graded

@[simp]

theorem Multiset.covBy_cons {α : Type u_1} (s : Multiset α) (a : α) : s ⋖ a ::ₘ s

theorem CovBy.exists_multiset_cons {α : Type u_1} {s t : Multiset α} (h : s ⋖ t) : ∃ (a : α), a ::ₘ s = t

theorem Multiset.covBy_iff {α : Type u_1} {s t : Multiset α} : s ⋖ t ↔ ∃ (a : α), a ::ₘ s = t

theorem CovBy.card_multiset {α : Type u_1} {s t : Multiset α} (h : s ⋖ t) : s.card ⋖ t.card

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}

@[instance_reducible]

instance Multiset.instGradeMinOrder {α : Type u_1} : GradeMinOrder ℕ (Multiset α)

Equations

• Multiset.instGradeMinOrder = { grade := Multiset.card, grade_strictMono := ⋯, covBy_grade := ⋯, isMin_grade := ⋯ }

@[simp]

theorem Multiset.grade_eq {α : Type u_1} (m : Multiset α) : grade ℕ m = m.card

theorem Finset.ordConnected_range_val {α : Type u_1} : (Set.range val).OrdConnected

Finsets form an order-connected suborder of multisets.

theorem Finset.ordConnected_range_coe {α : Type u_1} : (Set.range SetLike.coe).OrdConnected

Finsets form an order-connected suborder of sets.

@[simp]

theorem Finset.val_wcovBy_val {α : Type u_1} {s t : Finset α} : s.val ⩿ t.val ↔ s ⩿ t

@[simp]

theorem Finset.val_covBy_val {α : Type u_1} {s t : Finset α} : s.val ⋖ t.val ↔ s ⋖ t

@[simp]

theorem Finset.coe_wcovBy_coe {α : Type u_1} {s t : Finset α} : ↑s ⩿ ↑t ↔ s ⩿ t

@[simp]

theorem Finset.coe_covBy_coe {α : Type u_1} {s t : Finset α} : ↑s ⋖ ↑t ↔ s ⋖ t

theorem WCovBy.finset_val {α : Type u_1} {s t : Finset α} : s ⩿ t → s.val ⩿ t.val

Alias of the reverse direction of Finset.val_wcovBy_val.

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

Alias of the reverse direction of Finset.val_covBy_val.

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

Alias of the reverse direction of Finset.coe_wcovBy_coe.

theorem CovBy.finset_coe {α : Type u_1} {s t : Finset α} : s ⋖ t → ↑s ⋖ ↑t

Alias of the reverse direction of Finset.coe_covBy_coe.

@[simp]

theorem Finset.covBy_cons {α : Type u_1} {s : Finset α} {a : α} (ha : a ∉ s) : s ⋖ cons a s ha

theorem CovBy.exists_finset_cons {α : Type u_1} {s t : Finset α} (h : s ⋖ t) : ∃ (a : α) (ha : a ∉ s), Finset.cons a s ha = t

theorem Finset.covBy_iff_exists_cons {α : Type u_1} {s t : Finset α} : s ⋖ t ↔ ∃ (a : α) (ha : a ∉ s), cons a s ha = t

theorem CovBy.card_finset {α : Type u_1} {s 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 : α) : s.erase a ⩿ s

theorem Finset.covBy_insert {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] (ha : a ∉ s) : s ⋖ insert a s

@[simp]

theorem Finset.empty_covBy_singleton {α : Type u_1} (a : α) : ∅ ⋖ {a}

@[simp]

theorem Finset.erase_covBy {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] (ha : a ∈ s) : s.erase a ⋖ s

theorem CovBy.exists_finset_insert {α : Type u_1} {s t : Finset α} [DecidableEq α] (h : s ⋖ t) : ∃ a ∉ s, insert a s = t

theorem CovBy.exists_finset_erase {α : Type u_1} {s t : Finset α} [DecidableEq α] (h : s ⋖ t) : ∃ a ∈ t, t.erase a = s

theorem Finset.covBy_iff_exists_insert {α : Type u_1} {s t : Finset α} [DecidableEq α] : s ⋖ t ↔ ∃ a ∉ s, insert a s = t

theorem Finset.covBy_iff_card_sdiff_eq_one {α : Type u_1} {s t : Finset α} [DecidableEq α] : t ⋖ s ↔ t ⊆ s ∧ (s \ t).card = 1

theorem Finset.covBy_iff_exists_erase {α : Type u_1} {s t : Finset α} [DecidableEq α] : s ⋖ t ↔ ∃ a ∈ t, t.erase 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 : α) : IsCoatom {a}ᶜ

theorem Finset.isCoatom_iff {α : Type u_1} {s : Finset α} [Fintype α] [DecidableEq α] : IsCoatom s ↔ ∃ (a : α), s = {a}ᶜ

@[instance_reducible]

instance Finset.instGradeMinOrder_multiset {α : Type u_1} : GradeMinOrder (Multiset α) (Finset α)

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 := ⋯ }

@[simp]

theorem Finset.grade_multiset_eq {α : Type u_1} (s : Finset α) : grade (Multiset α) s = s.val

@[instance_reducible]

instance Finset.instGradeMinOrder_nat {α : Type u_1} : GradeMinOrder ℕ (Finset α)

Equations

• Finset.instGradeMinOrder_nat = { grade := Finset.card, grade_strictMono := ⋯, covBy_grade := ⋯, isMin_grade := ⋯ }

@[simp]

theorem Finset.grade_eq {α : Type u_1} (s : Finset α) : grade ℕ s = s.card