Documentation

Mathlib.Data.Set.MemPartition

Partitions based on membership of a sequence of sets #

Let f : ℕ → Set α be a sequence of sets. For n : ℕ, we can form the set of points that are in f 0 ∪ f 1 ∪ ... ∪ f (n-1); then the set of points in (f 0)ᶜ ∪ f 1 ∪ ... ∪ f (n-1) and so on for all 2^n choices of a set or its complement. The at most 2^n sets we obtain form a partition of univ : Set α. We call that partition memPartition f n (the membership partition of f). For n = 0 we set memPartition f 0 = {univ}.

The partition memPartition f (n + 1) is finer than memPartition f n.

Main definitions #

Main statements #

def memPartition {α : Type u_1} (f : Set α) :
Set (Set α)

memPartition f n is the partition containing at most 2^(n+1) sets, where each set contains the points that for all i belong to one of f i or its complement.

Equations
Instances For
    @[simp]
    theorem memPartition_zero {α : Type u_1} (f : Set α) :
    memPartition f 0 = {Set.univ}
    theorem memPartition_succ {α : Type u_1} (f : Set α) (n : ) :
    memPartition f (n + 1) = {s : Set α | umemPartition f n, s = u f n s = u \ f n}
    theorem disjoint_memPartition {α : Type u_1} (f : Set α) (n : ) {u : Set α} {v : Set α} (hu : u memPartition f n) (hv : v memPartition f n) (huv : u v) :
    @[simp]
    theorem sUnion_memPartition {α : Type u_1} (f : Set α) (n : ) :
    ⋃₀ memPartition f n = Set.univ
    theorem finite_memPartition {α : Type u_1} (f : Set α) (n : ) :
    (memPartition f n).Finite
    instance instFinite_memPartition {α : Type u_1} (f : Set α) (n : ) :
    Equations
    • =
    noncomputable instance instFintype_memPartition {α : Type u_1} (f : Set α) (n : ) :
    Equations
    def memPartitionSet {α : Type u_1} (f : Set α) :
    αSet α

    The set in memPartition f n to which a : α belongs.

    Equations
    Instances For
      @[simp]
      theorem memPartitionSet_zero {α : Type u_1} (f : Set α) (a : α) :
      memPartitionSet f 0 a = Set.univ
      theorem memPartitionSet_succ {α : Type u_1} (f : Set α) (n : ) (a : α) [Decidable (a f n)] :
      memPartitionSet f (n + 1) a = if a f n then memPartitionSet f n a f n else memPartitionSet f n a \ f n
      theorem memPartitionSet_mem {α : Type u_1} (f : Set α) (n : ) (a : α) :
      theorem mem_memPartitionSet {α : Type u_1} (f : Set α) (n : ) (a : α) :
      theorem memPartitionSet_eq_iff {α : Type u_1} {f : Set α} {n : } (a : α) {s : Set α} (hs : s memPartition f n) :
      memPartitionSet f n a = s a s
      theorem memPartitionSet_of_mem {α : Type u_1} {f : Set α} {n : } {a : α} {s : Set α} (hs : s memPartition f n) (ha : a s) :