omegaLimit_inter — Mathlib

English

The omega-limit is monotone with respect to intersection: the ω-limit of s1 ∩ s2 is contained in the intersection of the ω-limits.

Русский

ω‑лимит сохраняет пересечение: ω f ϕ (s1 ∩ s2) ⊆ ω f ϕ s1 ∩ ω f ϕ s2.

LaTeX

$$$ \omega f ϕ (s_1 \cap s_2) \subseteq \omega f ϕ s_1 \cap \omega f ϕ s_2. $$$

Lean4

theorem omegaLimit_inter : ω f ϕ (s₁ ∩ s₂) ⊆ ω f ϕ s₁ ∩ ω f ϕ s₂ :=
  subset_inter (omegaLimit_mono_right _ _ inter_subset_left) (omegaLimit_mono_right _ _ inter_subset_right)

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