subset_iInter₂ — Mathlib

English

Let s be a subset of α and t(i)(j) be a family of subsets of α indexed by i and j. If s ⊆ t(i)(j) for every i and j, then s is contained in the intersection of all t(i)(j), i.e. s ⊆ ⋂_i ⋂_j t(i)(j).

Русский

Пусть S ⊆ α и T(i)(j) — семейство подмножеств α, индексируемое по i и j. Если S ⊆ T(i)(j) для всех i, j, то S ⊆ ⋂_i ⋂_j T(i)(j).

LaTeX

$$$s \subseteq \bigcap_{i} \bigcap_{j} t(i)(j)$$$

Lean4

theorem subset_iInter₂ {s : Set α} {t : ∀ i, κ i → Set α} (h : ∀ i j, s ⊆ t i j) : s ⊆ ⋂ (i) (j), t i j :=
  subset_iInter fun x => subset_iInter <| h x

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