subset_of_biUnion_subset_biUnion — Mathlib

English

If a collection {f(i)}_{i∈s} is pairwise disjoint and each f(i) is nonempty, and the union over s is contained in the union over t, then s ⊆ t.

Русский

Если семейство {f(i)}_{i∈s} попарно непересекается и каждое f(i) непусто, а объединение по s вложено в объединение по t, то s ⊆ t.

LaTeX

$$$\\displaystyle \\Bigl(\\forall i,j\\in s, i\\neq j \\Rightarrow 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₀ : Pairwise (Disjoint on f)) (h₁ : ∀ i ∈ s, (f i).Nonempty)
    (h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i) : s ⊆ t :=
  Set.PairwiseDisjoint.subset_of_biUnion_subset_biUnion (h₀.set_pairwise _) h₁ h

Похожие утверждения