countablePartitionSet_eq_iff — Mathlib

English

Let hs be 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 countablePartitionSet_eq_iff {n : ℕ} (a : α) {s : Set α} (hs : s ∈ countablePartition α n) :
    countablePartitionSet n a = s ↔ a ∈ s :=
  memPartitionSet_eq_iff _ hs

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