omegaLimit_iInter — Mathlib

English

For a family of sets p i, the omega-limit of the intersection is contained in the intersection of the omega-limits: ω f ϕ (⋂ i, p i) ⊆ ⋂ i, ω f ϕ (p i).

Русский

Для семейства множеств {p_i} ω‑лимит пересечения содержится в пересечении ω‑лимитов: ω f ϕ (⋂ i, p_i) ⊆ ⋂ i, ω f ϕ (p_i).

LaTeX

$$$ \omega f ϕ (\bigcap_i p_i) \subseteq \bigcap_i \omega f ϕ (p_i). $$$

Lean4

theorem omegaLimit_iInter (p : ι → Set α) : ω f ϕ (⋂ i, p i) ⊆ ⋂ i, ω f ϕ (p i) :=
  subset_iInter fun _i ↦ omegaLimit_mono_right _ _ (iInter_subset _ _)

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