memPartitionSet — Mathlib

English

memPartitionSet(f,n,a) selects the unique block of memPartition(f,n) containing a.

Русский

memPartitionSet(f,n,a) выбирает единственный блок memPartition(f,n), содержащий a.

LaTeX

$$$\\operatorname{memPartitionSet}(f,n,a) \\in \\operatorname{memPartition}(f,n) \\quad \\text{and} \\quad a \\in \\operatorname{memPartitionSet}(f,n,a).$$$

Lean4

/-- The set in `memPartition f n` to which `a : α` belongs. -/
def memPartitionSet (f : ℕ → Set α) : ℕ → α → Set α
  | 0 => fun _ ↦ univ
  | n + 1 => fun a ↦ if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n

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