memPartition_succ — Mathlib

English

For n ≥ 0, memPartition(f)(n+1) consists of those sets obtained from memPartition(f)(n) by intersecting with f(n) or by removing f(n) from them.

Русский

Для n ≥ 0 memPartition(f)(n+1) состоит из таких подмножеств, которые получаются из memPartition(f)(n) путём пересечения с f(n) или удаления f(n) из них.

LaTeX

$$$\\operatorname{memPartition}(f)(n+1) = \\{ s \\mid \\exists u \\in \\operatorname{memPartition}(f)(n), s = u \\cap f(n) \\lor s = u \\setminus f(n) \\}$$$

Lean4

theorem memPartition_succ (f : ℕ → Set α) (n : ℕ) :
    memPartition f (n + 1) = {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} :=
  rfl

Похожие утверждения