omegaLimit_mono_right

Mathlib.Dynamics.OmegaLimit

URI: https://scilib.ai/kg/mathlib#omegaLimit_mono_right

← MathLib Explorer

English

If f1 ≤ f2 and s1 ⊆ s2, then ω f1 ϕ s1 ⊆ ω f2 ϕ s2.

Русский

Если f1 ≤ f2 и s1 ⊆ s2, то ω f1 ϕ s1 ⊆ ω f2 ϕ s2.

LaTeX

$$$$\omega f_1 ϕ s_1 \subseteq \omega f_2 ϕ s_2.$$$$

Lean4

theorem omegaLimit_mono_right {s₁ s₂ : Set α} (hs : s₁ ⊆ s₂) : ω f ϕ s₁ ⊆ ω f ϕ s₂ :=
  iInter₂_mono fun _u _hu ↦ closure_mono (image2_subset Subset.rfl hs)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru