English
For any a, s ∈ memPartition(f,n), memPartitionSet(f,n,a) = s if and only if a ∈ s.
Русский
Для любого a, s ∈ memPartition(f,n) выполнено: memPartitionSet(f,n,a) = s тогда и только если a ∈ s.
LaTeX
$$$\\forall a\\, \\forall s \\in \\operatorname{memPartition}(f,n),\\ \\operatorname{memPartitionSet}(f,n,a) = s \\iff a \\in s$$$
Lean4
theorem memPartitionSet_eq_iff {f : ℕ → Set α} {n : ℕ} (a : α) {s : Set α} (hs : s ∈ memPartition f n) :
memPartitionSet f n a = s ↔ a ∈ s :=
by
refine ⟨fun h ↦ h ▸ mem_memPartitionSet f n a, fun h ↦ ?_⟩
by_contra h_ne
have h_disj : Disjoint s (memPartitionSet f n a) :=
disjoint_memPartition f n hs (memPartitionSet_mem f n a) (Ne.symm h_ne)
refine absurd h_disj ?_
rw [not_disjoint_iff_nonempty_inter]
exact ⟨a, h, mem_memPartitionSet f n a⟩
