English
If the family {f(i)} is pairwise disjoint and every f(i) is nonempty, then the map s ↦ ⋃_{i∈s} f(i) from sets of indices to sets is injective.
Русский
Если семейство {f(i)} попарно непересекается и каждое f(i) непусто, тогда отображение s ↦ ⋃_{i∈s} f(i) из множеств индексов в множества является инъективным.
LaTeX
$$$\\mathrm{Injective}\\bigl(\\lambda s: \\{i:\\; i\\in s\\}\\mapsto \\bigcup_{i\\in s} f(i)\\bigr)$$$
Lean4
theorem biUnion_injective (h₀ : Pairwise (Disjoint on f)) (h₁ : ∀ i, (f i).Nonempty) :
Injective fun s : Set ι => ⋃ i ∈ s, f i := fun _s _t h =>
((h₀.subset_of_biUnion_subset_biUnion fun _ _ => h₁ _) <| h.subset).antisymm <|
(h₀.subset_of_biUnion_subset_biUnion fun _ _ => h₁ _) <| h.superset
