iInter_subset_iInter₂ — Mathlib

English

Let {s_i} be a family of subsets of a set α indexed by i in I, and for each i let κ(i) be an index set. Then the intersection over i of s_i is contained in the iterated intersection over i of the intersections over j in κ(i) of s_i.

Русский

Пусть {s_i} — семейство подмножеств α, индексируемое i ∈ I, и для каждого i задано κ(i) — множество индексов. Тогда ⋂_i s_i ⊆ ⋂_i ⋂_{j ∈ κ(i)} s_i.

LaTeX

$$$$ \\bigcap_{i} s_i \\subseteq \\bigcap_{i} \\bigcap_{j \\in \\kappa(i)} s_i $$$$

Lean4

theorem iInter_subset_iInter₂ (κ : ι → Sort*) (s : ι → Set α) : ⋂ i, s i ⊆ ⋂ (i) (_ : κ i), s i :=
  iInter_mono fun _ => subset_iInter fun _ => Subset.rfl

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