biUnion_mono — Mathlib

English

If s ⊆ s' and ∀ x ∈ s, t x ⊆ t' x, then ⋃ x ∈ s, t x ⊆ ⋃ x ∈ s', t' x.

Русский

Если s ⊆ s' и для всех x ∈ s выполняется t x ⊆ t' x, то ⋃ x ∈ s, t x ⊆ ⋃ x ∈ s', t' x.

LaTeX

$$$$ s \\subseteq s' \\Rightarrow \\bigcup_{x \\in s} t(x) \\subseteq \\bigcup_{x \\in s'} t'(x). $$$$

Lean4

theorem biUnion_mono {s s' : Set α} {t t' : α → Set β} (hs : s' ⊆ s) (h : ∀ x ∈ s, t x ⊆ t' x) :
    ⋃ x ∈ s', t x ⊆ ⋃ x ∈ s, t' x :=
  (biUnion_subset_biUnion_left hs).trans <| iUnion₂_mono h

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