English
If an element y lies in the union ⋃_{i∈s} f(i), then there exists a unique i ∈ s with y ∈ f(i).
Русский
Если элемент y принадлежит объединению ⋃_{i∈s} f(i), то существует единственный индекс i ∈ s с y ∈ f(i).
LaTeX
$$$y \\in \\bigcup_{i\\in s} f(i) \\Rightarrow \\exists! i\\,(i\\in s \\land y \\in f(i))$$$
Lean4
/-- In a disjoint union we can identify the unique set an element belongs to. -/
theorem pairwiseDisjoint_unique {y : α} (h_disjoint : PairwiseDisjoint s f) (hy : y ∈ (⋃ i ∈ s, f i)) :
∃! i, i ∈ s ∧ y ∈ f i := by
refine existsUnique_of_exists_of_unique ?ex ?unique
· simpa only [mem_iUnion, exists_prop] using hy
· rintro i j ⟨his, hi⟩ ⟨hjs, hj⟩
exact h_disjoint.elim his hjs <| not_disjoint_iff.mpr ⟨y, ⟨hi, hj⟩⟩
