English
Let f be a family of subsets, and s,t ⊆ indices. If the union over s is contained in the union over t, and all f(i) for i ∈ s are nonempty with the whole family on s∪t disjoint, then s ⊆ t.
Русский
Пусть имеется семейство подмножеств f и подмножества s,t индексов. Если объединение по s вложено в объединение по t, и все f(i) при i∈s непусты, а вся семья на s∪t попарно непересекается, тогда s ⊆ t.
LaTeX
$$$\\displaystyle \\Bigl(\\forall i,j\\in s\\, (f(i) \\cap f(j)) = \\emptyset\\Bigr) \\land \\Bigl(\\forall i\\in s, f(i) \\neq \\emptyset\\Bigr) \\land \\Bigl(\\bigcup_{i\\in s} f(i) \\subseteq \\bigcup_{i\\in t} f(i)\\Bigr) \\Rightarrow s \\subseteq t$$
Lean4
theorem subset_of_biUnion_subset_biUnion (h₀ : (s ∪ t).PairwiseDisjoint f) (h₁ : ∀ i ∈ s, (f i).Nonempty)
(h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i) : s ⊆ t := by
rintro i hi
obtain ⟨a, hai⟩ := h₁ i hi
obtain ⟨j, hj, haj⟩ := mem_iUnion₂.1 (h <| mem_iUnion₂_of_mem hi hai)
rwa [h₀.eq (subset_union_left hi) (subset_union_right hj) (not_disjoint_iff.2 ⟨a, hai, haj⟩)]
