Finite partition helpers

This file contains general-purpose constructions and facts about finite partitions: the partition of the top element into an element and its complement, the associated indexed partition, cardinality bounds for common refinements, and the behavior of intersections of parts under refinement.

noncomputable def Finpartition.bipartition {α : Type u_1} [BooleanAlgebra α] [DecidableEq α] (s : α) : Finpartition ⊤

The finite partition of the top element into an element and its complement, omitting either part when it is bottom.

Equations

• Finpartition.bipartition s = (Finpartition.ofPairwiseDisjoint {s, sᶜ} ⋯).copy ⋯

@[simp]

theorem Finpartition.parts_bipartition {α : Type u_1} [BooleanAlgebra α] [DecidableEq α] (s : α) : (bipartition s).parts = {s, sᶜ}.erase ⊥

theorem Finpartition.card_parts_bipartition_le {α : Type u_1} [BooleanAlgebra α] [DecidableEq α] (s : α) : (bipartition s).parts.card ≤ 2

A bipartition has at most two parts.

theorem Finpartition.mem_bipartition_of_ne_bot {α : Type u_1} [BooleanAlgebra α] [DecidableEq α] {s : α} (hs : s ≠ ⊥) : s ∈ (bipartition s).parts

A non-bottom element is a part of its bipartition.

theorem Finpartition.card_parts_inf_le_mul {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} (P Q : Finpartition a) : (P ⊓ Q).parts.card ≤ P.parts.card * Q.parts.card

The number of parts in a common refinement is at most the product of the two part counts.

noncomputable def Finpartition.indexedPartition {Ω : Type u_1} (P : Finpartition Set.univ) : IndexedPartition fun (p : ↥P.parts) => ↑p

The indexed partition associated to a finite partition of Set.univ, indexed by its actual parts. Its index sends each point to the unique part containing it.

Equations

• P.indexedPartition = IndexedPartition.mk' (fun (p : ↥P.parts) => ↑p) ⋯ ⋯ ⋯

theorem Finpartition.inter_part_eq_self_or_eq_empty_of_le {Ω : Type u_1} {u : Set Ω} {P Q : Finpartition u} (href : Q ≤ P) {r : Set Ω} (hr : r ∈ Q.parts) {p : Set Ω} (hp : p ∈ P.parts) : r ∩ p = r ∨ r ∩ p = ∅

Under refinement, a part of the finer partition is either contained in a given part of the coarser one or disjoint from it.