countablePartitionSet — Mathlib

English

countablePartitionSet(n,a) is the block of countablePartition α n that contains a; i.e., it is a member of countablePartition α n and contains a.

Русский

countablePartitionSet(n,a) есть блок countablePartition α n, который содержит a; то есть он является элементом countablePartition α n и содержит a.

LaTeX

$$$$ countablePartitionSet\\,n\\,a \\in countablePartition\\,\\alpha\\,n \\;\\land\\; a \\in countablePartitionSet\\,n\\,a. $$$$

Lean4

/-- The set in `countablePartition α n` to which `a : α` belongs. -/
def countablePartitionSet (n : ℕ) (a : α) : Set α :=
  memPartitionSet (enumerateCountable countable_countableGeneratingSet ∅) n a

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