English
The block containing a at level n+1 is obtained from the block at level n by either intersecting with f(n) if a ∈ f(n), or by removing f(n) if a ∉ f(n).
Русский
Блок, содержащий a на уровне n+1, получается из блока на уровне n путём пересечения с f(n) при условии a ∈ f(n), или удаления f(n) при a ∉ f(n).
LaTeX
$$$\\operatorname{memPartitionSet}(f,n+1,a) = \\begin{cases} \\operatorname{memPartitionSet}(f,n,a) \\cap f(n), & a \\in f(n) \\\\ \\operatorname{memPartitionSet}(f,n,a) \\setminus f(n), & a \\notin f(n) \\end{cases}$$$
Lean4
theorem memPartitionSet_succ (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 := by
simp [memPartitionSet]
