# 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

source
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

- memPartition f 0 = {Set.univ}
- memPartition f n.succ = {s : Set α | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}

Instances For

source
@[simp]
theorem memPartition_zero {α : Type u_1} (f : ℕ → Set α) :
memPartition f 0 = {Set.univ}
source
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}
source
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
source
@[simp]
theorem sUnion_memPartition {α : Type u_1} (f : ℕ → Set α) (n : ℕ) :
⋃₀ memPartition f n = Set.univ
source
theorem finite_memPartition {α : Type u_1} (f : ℕ → Set α) (n : ℕ) :
(memPartition f n).Finite
source
instance instFinite_memPartition {α : Type u_1} (f : ℕ → Set α) (n : ℕ) :
Finite ↑(memPartition f n)
source
noncomputable instance instFintype_memPartition {α : Type u_1} (f : ℕ → Set α) (n : ℕ) :
Fintype ↑(memPartition f n)
Equations

- instFintype_memPartition f n = ⋯.fintype

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

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

Equations

- memPartitionSet f 0 = fun (x : α) => Set.univ
- memPartitionSet f n.succ = fun (a : α) => if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n

Instances For

source
@[simp]
theorem memPartitionSet_zero {α : Type u_1} (f : ℕ → Set α) (a : α) :
memPartitionSet f 0 a = Set.univ
source
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
source
theorem memPartitionSet_mem {α : Type u_1} (f : ℕ → Set α) (n : ℕ) (a : α) :
memPartitionSet f n a ∈ memPartition f n
source
theorem mem_memPartitionSet {α : Type u_1} (f : ℕ → Set α) (n : ℕ) (a : α) :
a ∈ memPartitionSet f n a
source
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
source
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