omegaLimit_mono_left

Mathlib.Dynamics.OmegaLimit

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

English

If f1 ≤ f2, then ω f1 ϕ s ⊆ ω f2 ϕ s.

Русский

Если f1 ≤ f2, то ω-предел слева вложен в ω-предел справа.

LaTeX

$$$$\omega f_1 ϕ s \subseteq \omega f_2 ϕ s.$$$$

Lean4

theorem omegaLimit_mono_left {f₁ f₂ : Filter τ} (hf : f₁ ≤ f₂) : ω f₁ ϕ s ⊆ ω f₂ ϕ s :=
  omegaLimit_subset_of_tendsto ϕ s (tendsto_id'.2 hf)

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

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

Разделы

Аффилиация

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