isClosed_omegaLimit

Mathlib.Dynamics.OmegaLimit

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

English

If s1 ⊆ s2, then ω f ϕ s1 ⊆ ω f ϕ s2.

Русский

Если s1 ⊆ s2, то ω-предел для s1 вложен в ω-предел для s2.

LaTeX

$$$$\omega f ϕ s_1 \subseteq \omega f ϕ s_2.$$$$

Lean4

theorem isClosed_omegaLimit : IsClosed (ω f ϕ s) :=
  isClosed_iInter fun _u ↦ isClosed_iInter fun _hu ↦ isClosed_closure

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

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

Разделы

Аффилиация

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