English
Let s: ℕ → Set α and H x a witness that every x lies in some s n. For each n, the preimage of the singleton {n} under x ↦ Nat.find (H x) equals disjointed s n.
Русский
Пусть s: ℕ → множество, и существует доказательство, что каждый x принадлежит некоторому s n. Тогда предобраз элемента {n} под x ↦ Nat.find(H x) равен disjointed s n.
LaTeX
$$$(\forall x, \exists n, x \in s n) \Rightarrow \dots$; "preimage" formula: $\{ x : α \mid \operatorname{Nat.find}(H x) = n \} = \operatorname{disjointed} s n$$$
Lean4
theorem preimage_find_eq_disjointed (s : ℕ → Set α) (H : ∀ x, ∃ n, x ∈ s n) [∀ x n, Decidable (x ∈ s n)] (n : ℕ) :
(fun x => Nat.find (H x)) ⁻¹' { n } = disjointed s n :=
by
ext x
simp [Nat.find_eq_iff, disjointed_eq_inter_compl]
