mem_countablePartitionSet — Mathlib

English

If hs holds that s ∈ countablePartition α n, then countablePartitionSet n a = s iff a ∈ s.

Русский

Пусть hs: s ∈ countablePartition α n, тогда countablePartitionSet n a = s тогда и только если a ∈ s.

LaTeX

$$$$ s \\in countablePartition\\,\\alpha\\,n \\Rightarrow (countablePartitionSet\\,n\\,a = s \\iff a \\in s). $$$$

Lean4

theorem mem_countablePartitionSet (n : ℕ) (a : α) : a ∈ countablePartitionSet n a :=
  mem_memPartitionSet _ _ _

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