English
Define memPartition(f) by: (i) memPartition(f)(0) = { univ }; (ii) memPartition(f)(n+1) = { s ⊆ α | ∃ u ∈ memPartition(f)(n), s = u ∩ f(n) or s = u \\ f(n) } for n ≥ 0. This yields a partition of α into at most 2^(n+1) blocks, each block determined by choosing, for each i ≤ n, whether to take f(i) or its complement.
Русский
Определим memPartition(f) рекурсивно: (i) memPartition(f)(0) = {univ}; (ii) memPartition(f)(n+1) = { s ⊆ α | ∃ u ∈ memPartition(f)(n), s = u ∩ f(n) или s = u \\ f(n) }. Это—разбиение α на не более чем 2^(n+1) частей, каждая часть определяется выбором на каждом шаге f(i) или комплемента.
LaTeX
$$$\\operatorname{memPartition}(f)(0) = \\{\\operatorname{univ}\\}, \\\\ \\operatorname{memPartition}(f)(n+1) = \\{ s \\subseteq \\alpha \\mid \\exists u \\in \\operatorname{memPartition}(f)(n), s = u \\cap f(n) \\ \\lor\\ s = u \\setminus f(n) \\}.$$$
Lean4
/-- `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. -/
def memPartition (f : ℕ → Set α) : ℕ → Set (Set α)
| 0 => { univ }
| n + 1 => {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
