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 #

source
@[simp]
theorem Multiset.covBy_cons {α : Type u_1} (s : Multiset α) (a : α) :
s ⋖ a ::ₘ s
source
theorem CovBy.exists_multiset_cons {α : Type u_1} {s t : Multiset α} (h : s ⋖ t) :
∃ (a : α), a ::ₘ s = t
source
theorem Multiset.covBy_iff {α : Type u_1} {s t : Multiset α} :
s ⋖ t ↔ ∃ (a : α), a ::ₘ s = t
source
theorem CovBy.card_multiset {α : Type u_1} {s t : Multiset α} (h : s ⋖ t) :
s.card ⋖ t.card
source
theorem Multiset.isAtom_iff {α : Type u_1} {s : Multiset α} :
IsAtom s ↔ ∃ (a : α), s = {a}
source
@[simp]
theorem Multiset.isAtom_singleton {α : Type u_1} (a : α) :
IsAtom {a}
source
instance Multiset.instGradeMinOrder {α : Type u_1} :
GradeMinOrder ℕ (Multiset α)
Equations
    source
    @[simp]
    theorem Multiset.grade_eq {α : Type u_1} (m : Multiset α) :
    grade ℕ m = m.card
    source
    theorem Finset.ordConnected_range_val {α : Type u_1} :
    (Set.range val).OrdConnected

    Finsets form an order-connected suborder of multisets.

    source
    theorem Finset.ordConnected_range_coe {α : Type u_1} :
    (Set.range toSet).OrdConnected

    Finsets form an order-connected suborder of sets.

    source
    @[simp]
    theorem Finset.val_wcovBy_val {α : Type u_1} {s t : Finset α} :
    s.val ⩿ t.val ↔ s ⩿ t
    source
    @[simp]
    theorem Finset.val_covBy_val {α : Type u_1} {s t : Finset α} :
    s.val ⋖ t.val ↔ s ⋖ t
    source
    @[simp]
    theorem Finset.coe_wcovBy_coe {α : Type u_1} {s t : Finset α} :
    ↑s ⩿ ↑t ↔ s ⩿ t
    source
    @[simp]
    theorem Finset.coe_covBy_coe {α : Type u_1} {s t : Finset α} :
    ↑s ⋖ ↑t ↔ s ⋖ t
    source
    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.

    source
    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.

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

    Alias of the reverse direction of Finset.coe_wcovBy_coe.

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

    Alias of the reverse direction of Finset.coe_covBy_coe.

    source
    @[simp]
    theorem Finset.covBy_cons {α : Type u_1} {s : Finset α} {a : α} (ha : a ∉ s) :
    s ⋖ cons a s ha
    source
    theorem CovBy.exists_finset_cons {α : Type u_1} {s t : Finset α} (h : s ⋖ t) :
    ∃ (a : α) (ha : a ∉ s), Finset.cons a s ha = t
    source
    theorem Finset.covBy_iff_exists_cons {α : Type u_1} {s t : Finset α} :
    s ⋖ t ↔ ∃ (a : α) (ha : a ∉ s), cons a s ha = t
    source
    theorem CovBy.card_finset {α : Type u_1} {s t : Finset α} (h : s ⋖ t) :
    s.card ⋖ t.card
    source
    @[simp]
    theorem Finset.wcovBy_insert {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
    s ⩿ insert a s
    source
    @[simp]
    theorem Finset.erase_wcovBy {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
    s.erase a ⩿ s
    source
    theorem Finset.covBy_insert {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] (ha : a ∉ s) :
    s ⋖ insert a s
    source
    @[simp]
    theorem Finset.erase_covBy {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] (ha : a ∈ s) :
    s.erase a ⋖ s
    source
    theorem CovBy.exists_finset_insert {α : Type u_1} {s t : Finset α} [DecidableEq α] (h : s ⋖ t) :
    ∃ a ∉ s, insert a s = t
    source
    theorem CovBy.exists_finset_erase {α : Type u_1} {s t : Finset α} [DecidableEq α] (h : s ⋖ t) :
    ∃ a ∈ t, t.erase a = s
    source
    theorem Finset.covBy_iff_exists_insert {α : Type u_1} {s t : Finset α} [DecidableEq α] :
    s ⋖ t ↔ ∃ a ∉ s, insert a s = t
    source
    theorem Finset.covBy_iff_card_sdiff_eq_one {α : Type u_1} {s t : Finset α} [DecidableEq α] :
    t ⋖ s ↔ t ⊆ s ∧ (s \ t).card = 1
    source
    theorem Finset.covBy_iff_exists_erase {α : Type u_1} {s t : Finset α} [DecidableEq α] :
    s ⋖ t ↔ ∃ a ∈ t, t.erase a = s
    source
    @[simp]
    theorem Finset.isAtom_singleton {α : Type u_1} (a : α) :
    IsAtom {a}
    source
    theorem Finset.isAtom_iff {α : Type u_1} {s : Finset α} :
    IsAtom s ↔ ∃ (a : α), s = {a}
    source
    theorem Finset.isCoatom_compl_singleton {α : Type u_1} [Fintype α] [DecidableEq α] (a : α) :
    IsCoatom {a}ᶜ
    source
    theorem Finset.isCoatom_iff {α : Type u_1} {s : Finset α} [Fintype α] [DecidableEq α] :
    IsCoatom s ↔ ∃ (a : α), s = {a}ᶜ
    source
    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
      source
      @[simp]
      theorem Finset.grade_multiset_eq {α : Type u_1} (s : Finset α) :
      grade (Multiset α) s = s.val
      source
      instance Finset.instGradeMinOrder_nat {α : Type u_1} :
      GradeMinOrder ℕ (Finset α)
      Equations
        source
        @[simp]
        theorem Finset.grade_eq {α : Type u_1} (s : Finset α) :
        grade ℕ s = s.card