subset_iInter_iff — Mathlib

English

For a family t_i of subsets, s ⊆ ⋂_i t_i holds if and only if s ⊆ t_i for every i.

Русский

Для семейства множеств t_i верно, что s ⊆ ⋂_i t_i тогда и только тогда, когда s ⊆ t_i для каждого i.

LaTeX

$$$s \subseteq \bigcap_i t_i \iff \forall i,\ s \subseteq t_i$$$

Lean4

@[simp]
theorem subset_iInter_iff {s : Set α} {t : ι → Set α} : (s ⊆ ⋂ i, t i) ↔ ∀ i, s ⊆ t i :=
  le_iInf_iff

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