subset_iUnion₂_of_subset — Mathlib

English

If s ⊆ t i j for some i, j, then s ⊆ ⋃ (i) (j), t i j.

Русский

Если s ⊆ t_{i j} для некоторых i, j, то s ⊆ ⋃_{i,j} t_{i j}.

LaTeX

$$$\text{(exists } i,j) \ s \subseteq t_{ij} \implies s \subseteq \bigcup_{i,j} t_{ij}$$$

Lean4

/-- This rather trivial consequence of `subset_iUnion₂` is convenient with `apply`, and has `i` and
`j` explicit for this purpose. -/
theorem subset_iUnion₂_of_subset {s : Set α} {t : ∀ i, κ i → Set α} (i : ι) (j : κ i) (h : s ⊆ t i j) :
    s ⊆ ⋃ (i) (j), t i j :=
  le_iSup₂_of_le i j h

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