Documentation

Mathlib.Order.Partition.Finpartition

Finite partitions #

In this file, we define finite partitions. A finpartition of a : α is a finite set of pairwise disjoint parts parts : Finset α which does not contain and whose supremum is a.

Finpartitions of a finset are at the heart of Szemerédi's regularity lemma. They are also studied purely order theoretically in Sperner theory.

Constructions #

We provide many ways to build finpartitions:

Finpartition.indiscrete and Finpartition.bind together form the monadic structure of Finpartition.

Implementation notes #

Forbidding as a part follows mathematical tradition and is a pragmatic choice concerning operations on Finpartition. Not caring about being a part or not breaks extensionality (it's not because the parts of P and the parts of Q have the same elements that P = Q). Enforcing to be a part makes Finpartition.bind uglier and doesn't rid us of the need of Finpartition.ofErase.

TODO #

The order is the wrong way around to make Finpartition a a graded order. Is it bad to depart from the literature and turn the order around?

theorem Finpartition.ext {α : Type u_1} :
∀ {inst : Lattice α} {inst_1 : OrderBot α} {a : α} (x y : Finpartition a), x.parts = y.partsx = y
theorem Finpartition.ext_iff {α : Type u_1} :
∀ {inst : Lattice α} {inst_1 : OrderBot α} {a : α} (x y : Finpartition a), x = y x.parts = y.parts
structure Finpartition {α : Type u_1} [Lattice α] [OrderBot α] (a : α) :
Type u_1

A finite partition of a : α is a pairwise disjoint finite set of elements whose supremum is a. We forbid as a part.

  • parts : Finset α

    The elements of the finite partition of a

  • supIndep : self.parts.SupIndep id

    The partition is supremum-independent

  • sup_parts : self.parts.sup id = a

    The supremum of the partition is a

  • not_bot_mem : self.parts

    No element of the partition is bottom

Instances For
    theorem Finpartition.supIndep {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (self : Finpartition a) :
    self.parts.SupIndep id

    The partition is supremum-independent

    theorem Finpartition.sup_parts {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (self : Finpartition a) :
    self.parts.sup id = a

    The supremum of the partition is a

    theorem Finpartition.not_bot_mem {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (self : Finpartition a) :
    self.parts

    No element of the partition is bottom

    instance instDecidableEqFinpartition :
    {α : Type u_2} → {inst : Lattice α} → {inst_1 : OrderBot α} → {a : α} → [inst_2 : DecidableEq α] → DecidableEq (Finpartition a)
    Equations
    • instDecidableEqFinpartition = decEqFinpartition✝
    @[simp]
    theorem Finpartition.ofErase_parts {α : Type u_1} [Lattice α] [OrderBot α] [DecidableEq α] {a : α} (parts : Finset α) (sup_indep : parts.SupIndep id) (sup_parts : parts.sup id = a) :
    (Finpartition.ofErase parts sup_indep sup_parts).parts = parts.erase
    def Finpartition.ofErase {α : Type u_1} [Lattice α] [OrderBot α] [DecidableEq α] {a : α} (parts : Finset α) (sup_indep : parts.SupIndep id) (sup_parts : parts.sup id = a) :

    A Finpartition constructor which does not insist on not being a part.

    Equations
    • Finpartition.ofErase parts sup_indep sup_parts = { parts := parts.erase , supIndep := , sup_parts := , not_bot_mem := }
    Instances For
      @[simp]
      theorem Finpartition.ofSubset_parts {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {b : α} (P : Finpartition a) {parts : Finset α} (subset : parts P.parts) (sup_parts : parts.sup id = b) :
      (P.ofSubset subset sup_parts).parts = parts
      def Finpartition.ofSubset {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {b : α} (P : Finpartition a) {parts : Finset α} (subset : parts P.parts) (sup_parts : parts.sup id = b) :

      A Finpartition constructor from a bigger existing finpartition.

      Equations
      • P.ofSubset subset sup_parts = { parts := parts, supIndep := , sup_parts := sup_parts, not_bot_mem := }
      Instances For
        @[simp]
        theorem Finpartition.copy_parts {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {b : α} (P : Finpartition a) (h : a = b) :
        (P.copy h).parts = P.parts
        def Finpartition.copy {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {b : α} (P : Finpartition a) (h : a = b) :

        Changes the type of a finpartition to an equal one.

        Equations
        • P.copy h = { parts := P.parts, supIndep := , sup_parts := , not_bot_mem := }
        Instances For
          def Finpartition.map {α : Type u_1} [Lattice α] [OrderBot α] {β : Type u_2} [Lattice β] [OrderBot β] {a : α} (e : α ≃o β) (P : Finpartition a) :

          Transfer a finpartition over an order isomorphism.

          Equations
          Instances For
            @[simp]
            theorem Finpartition.parts_map {α : Type u_1} [Lattice α] [OrderBot α] {β : Type u_2} [Lattice β] [OrderBot β] {a : α} {e : α ≃o β} {P : Finpartition a} :
            (Finpartition.map e P).parts = Finset.map (e).toEmbedding P.parts
            @[simp]
            theorem Finpartition.empty_parts (α : Type u_1) [Lattice α] [OrderBot α] :

            The empty finpartition.

            Equations
            Instances For
              @[simp]
              theorem Finpartition.default_eq_empty (α : Type u_1) [Lattice α] [OrderBot α] :
              @[simp]
              theorem Finpartition.indiscrete_parts {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (ha : a ) :
              (Finpartition.indiscrete ha).parts = {a}
              def Finpartition.indiscrete {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (ha : a ) :

              The finpartition in one part, aka indiscrete finpartition.

              Equations
              Instances For
                theorem Finpartition.le {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (P : Finpartition a) {b : α} (hb : b P.parts) :
                b a
                theorem Finpartition.ne_bot {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (P : Finpartition a) {b : α} (hb : b P.parts) :
                theorem Finpartition.disjoint {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (P : Finpartition a) :
                (P.parts).PairwiseDisjoint id
                theorem Finpartition.parts_eq_empty_iff {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {P : Finpartition a} :
                P.parts = a =
                theorem Finpartition.parts_nonempty_iff {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {P : Finpartition a} :
                P.parts.Nonempty a
                theorem Finpartition.parts_nonempty {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (P : Finpartition a) (ha : a ) :
                P.parts.Nonempty
                Equations
                • Finpartition.instUniqueBot = let __src := inferInstance; { toInhabited := __src, uniq := }
                @[reducible, inline]
                abbrev IsAtom.uniqueFinpartition {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {P : Finpartition a} (ha : IsAtom a) :

                There's a unique partition of an atom.

                Equations
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.

                  Refinement order #

                  instance Finpartition.instLE {α : Type u_1} [Lattice α] [OrderBot α] {a : α} :

                  We say that P ≤ Q if P refines Q: each part of P is less than some part of Q.

                  Equations
                  • Finpartition.instLE = { le := fun (P Q : Finpartition a) => ∀ ⦃b : α⦄, b P.partscQ.parts, b c }
                  instance Finpartition.instPartialOrder {α : Type u_1} [Lattice α] [OrderBot α] {a : α} :
                  Equations
                  Equations
                  theorem Finpartition.parts_top_subset {α : Type u_1} [Lattice α] [OrderBot α] (a : α) [Decidable (a = )] :
                  .parts {a}
                  theorem Finpartition.parts_top_subsingleton {α : Type u_1} [Lattice α] [OrderBot α] (a : α) [Decidable (a = )] :
                  (.parts).Subsingleton
                  instance Finpartition.instInf {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} :
                  Equations
                  @[simp]
                  theorem Finpartition.parts_inf {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} (P : Finpartition a) (Q : Finpartition a) :
                  (P Q).parts = (Finset.image (fun (bc : α × α) => bc.1 bc.2) (P.parts ×ˢ Q.parts)).erase
                  Equations
                  • Finpartition.instSemilatticeInf = let __src := inferInstance; let __src_1 := inferInstance; SemilatticeInf.mk
                  theorem Finpartition.exists_le_of_le {α : Type u_1} [DistribLattice α] [OrderBot α] {a : α} {b : α} {P : Finpartition a} {Q : Finpartition a} (h : P Q) (hb : b Q.parts) :
                  cP.parts, c b
                  theorem Finpartition.card_mono {α : Type u_1} [DistribLattice α] [OrderBot α] {a : α} {P : Finpartition a} {Q : Finpartition a} (h : P Q) :
                  Q.parts.card P.parts.card
                  @[simp]
                  theorem Finpartition.bind_parts {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} (P : Finpartition a) (Q : (i : α) → i P.partsFinpartition i) :
                  (P.bind Q).parts = P.parts.attach.biUnion fun (i : { x : α // x P.parts }) => (Q i ).parts
                  def Finpartition.bind {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} (P : Finpartition a) (Q : (i : α) → i P.partsFinpartition i) :

                  Given a finpartition P of a and finpartitions of each part of P, this yields the finpartition of a obtained by juxtaposing all the subpartitions.

                  Equations
                  • P.bind Q = { parts := P.parts.attach.biUnion fun (i : { x : α // x P.parts }) => (Q i ).parts, supIndep := , sup_parts := , not_bot_mem := }
                  Instances For
                    theorem Finpartition.mem_bind {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} {b : α} {P : Finpartition a} {Q : (i : α) → i P.partsFinpartition i} :
                    b (P.bind Q).parts ∃ (A : α) (hA : A P.parts), b (Q A hA).parts
                    theorem Finpartition.card_bind {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} {P : Finpartition a} (Q : (i : α) → i P.partsFinpartition i) :
                    (P.bind Q).parts.card = P.parts.attach.sum fun (A : { x : α // x P.parts }) => (Q A ).parts.card
                    @[simp]
                    theorem Finpartition.extend_parts {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} {b : α} {c : α} (P : Finpartition a) (hb : b ) (hab : Disjoint a b) (hc : a b = c) :
                    (P.extend hb hab hc).parts = insert b P.parts
                    def Finpartition.extend {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} {b : α} {c : α} (P : Finpartition a) (hb : b ) (hab : Disjoint a b) (hc : a b = c) :

                    Adds b to a finpartition of a to make a finpartition of a ⊔ b.

                    Equations
                    • P.extend hb hab hc = { parts := insert b P.parts, supIndep := , sup_parts := , not_bot_mem := }
                    Instances For
                      theorem Finpartition.card_extend {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} (P : Finpartition a) (b : α) (c : α) {hb : b } {hab : Disjoint a b} {hc : a b = c} :
                      (P.extend hb hab hc).parts.card = P.parts.card + 1
                      @[simp]
                      theorem Finpartition.avoid_parts_val {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableEq α] {a : α} (P : Finpartition a) (b : α) :
                      (P.avoid b).parts.val = (Multiset.map (fun (x : α) => x \ b) P.parts.val).dedup.erase
                      def Finpartition.avoid {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableEq α] {a : α} (P : Finpartition a) (b : α) :

                      Restricts a finpartition to avoid a given element.

                      Equations
                      Instances For
                        @[simp]
                        theorem Finpartition.mem_avoid {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableEq α] {a : α} {b : α} {c : α} (P : Finpartition a) :
                        c (P.avoid b).parts dP.parts, ¬d b d \ b = c

                        Finite partitions of finsets #

                        theorem Finpartition.nonempty_of_mem_parts {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : Finset α} (ha : a P.parts) :
                        a.Nonempty
                        theorem Finpartition.eq_of_mem_parts {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (P : Finpartition s) {a : α} (ht : t P.parts) (hu : u P.parts) (hat : a t) (hau : a u) :
                        t = u
                        theorem Finpartition.exists_mem {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α} (ha : a s) :
                        tP.parts, a t
                        theorem Finpartition.biUnion_parts {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) :
                        P.parts.biUnion id = s
                        theorem Finpartition.existsUnique_mem {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α} (ha : a s) :
                        ∃! t : Finset α, t P.parts a t
                        def Finpartition.part {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) (a : α) :

                        The part of the finpartition that a lies in.

                        Equations
                        Instances For
                          theorem Finpartition.part_mem {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α} (ha : a s) :
                          P.part a P.parts
                          theorem Finpartition.mem_part {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α} (ha : a s) :
                          a P.part a
                          theorem Finpartition.part_surjOn {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) :
                          Set.SurjOn P.part s P.parts
                          theorem Finpartition.exists_subset_part_bijOn {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) :
                          rs, Set.BijOn P.part r P.parts
                          theorem Finpartition.sum_card_parts {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) :
                          (P.parts.sum fun (i : Finset α) => i.card) = s.card
                          instance Finpartition.instBotFinset {α : Type u_1} [DecidableEq α] (s : Finset α) :

                          is the partition in singletons, aka discrete partition.

                          Equations
                          @[simp]
                          theorem Finpartition.parts_bot {α : Type u_1} [DecidableEq α] (s : Finset α) :
                          .parts = Finset.map { toFun := singleton, inj' := } s
                          theorem Finpartition.card_bot {α : Type u_1} [DecidableEq α] (s : Finset α) :
                          .parts.card = s.card
                          theorem Finpartition.mem_bot_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} :
                          t .parts as, {a} = t
                          Equations
                          theorem Finpartition.card_parts_le_card {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) :
                          P.parts.card s.card
                          def Finpartition.ofSetoid {α : Type u_1} [DecidableEq α] [Fintype α] (s : Setoid α) [DecidableRel Setoid.r] :
                          Finpartition Finset.univ

                          A setoid over a finite type induces a finpartition of the type's elements, where the parts are the setoid's equivalence classes.

                          Equations
                          Instances For
                            theorem Finpartition.mem_part_ofSetoid_iff_rel {α : Type u_1} [DecidableEq α] {a : α} [Fintype α] {s : Setoid α} [DecidableRel Setoid.r] {b : α} :
                            def Finpartition.atomise {α : Type u_1} [DecidableEq α] [Fintype α] (s : Finset α) (F : Finset (Finset α)) :

                            Cuts s along the finsets in F: Two elements of s will be in the same part if they are in the same finsets of F.

                            Equations
                            Instances For
                              theorem Finpartition.mem_atomise {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} [Fintype α] {F : Finset (Finset α)} :
                              t (Finpartition.atomise s F).parts t.Nonempty QF, Finset.filter (fun (i : α) => uF, u Q i u) s = t
                              theorem Finpartition.atomise_empty {α : Type u_1} [DecidableEq α] {s : Finset α} [Fintype α] (hs : s.Nonempty) :
                              (Finpartition.atomise s ).parts = {s}
                              theorem Finpartition.card_atomise_le {α : Type u_1} [DecidableEq α] {s : Finset α} [Fintype α] {F : Finset (Finset α)} :
                              (Finpartition.atomise s F).parts.card 2 ^ F.card
                              theorem Finpartition.biUnion_filter_atomise {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} [Fintype α] {F : Finset (Finset α)} (ht : t F) (hts : t s) :
                              (Finset.filter (fun (u : Finset α) => u t u.Nonempty) (Finpartition.atomise s F).parts).biUnion id = t
                              theorem Finpartition.card_filter_atomise_le_two_pow {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} [Fintype α] {F : Finset (Finset α)} (ht : t F) :
                              (Finset.filter (fun (u : Finset α) => u t u.Nonempty) (Finpartition.atomise s F).parts).card 2 ^ (F.card - 1)