countablePartitionSet_mem — Mathlib

English

The block countablePartitionSet(n,a) belongs to the partition: countablePartitionSet n a ∈ countablePartition α n.

Русский

Блок countablePartitionSet(n,a) принадлежит разбиению: countablePartitionSet n a ∈ countablePartition α n.

LaTeX

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

Lean4

theorem countablePartitionSet_mem (n : ℕ) (a : α) : countablePartitionSet n a ∈ countablePartition α n :=
  memPartitionSet_mem _ _ _

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