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

• memPartition f n: the membership partition of the first n sets in f.
• memPartitionSet: memPartitionSet f n x is the set in the partition memPartition f n to which x belongs.

Main statements

• disjoint_memPartition: the sets in memPartition f n are disjoint
• sUnion_memPartition: the union of the sets in memPartition f n is univ
• finite_memPartition: memPartition f n is finite

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.

@[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 α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}

theorem disjoint_memPartition {α : Type u_1} (f : ℕ → Set α) (n : ℕ) {u v : Set α} (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v) : Disjoint 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 : ℕ) : Finite ↑(memPartition f n)

noncomputable instance instFintype_memPartition {α : Type u_1} (f : ℕ → Set α) (n : ℕ) : Fintype ↑(memPartition f n)

def memPartitionSet {α : Type u_1} (f : ℕ → Set α) : ℕ → α → Set α

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

@[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 : α) : memPartitionSet f n a ∈ memPartition f n

theorem mem_memPartitionSet {α : Type u_1} (f : ℕ → Set α) (n : ℕ) (a : α) : a ∈ memPartitionSet f 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) : memPartitionSet f n a = s