iInter₂_subset_of_subset — Mathlib

English

If s(i)(j) ⊆ t, then ⋂_{i} ⋂_{j} s(i)(j) ⊆ t.

Русский

Если s(i)(j) ⊆ t для всех i, j, то ⋂_{i} ⋂_{j} s(i)(j) ⊆ t.

LaTeX

$$$\bigcap_{i} \bigcap_{j} s_{ij} \subseteq t \quad \text{if } s_{ij} \subseteq t \text{ for all } i,j$$$

Lean4

/-- This rather trivial consequence of `iInter₂_subset` is convenient with `apply`, and has `i` and
`j` explicit for this purpose. -/
theorem iInter₂_subset_of_subset {s : ∀ i, κ i → Set α} {t : Set α} (i : ι) (j : κ i) (h : s i j ⊆ t) :
    ⋂ (i) (j), s i j ⊆ t :=
  iInf₂_le_of_le i j h

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