eventually_eventuallyLE_nhds

Mathlib.Topology.Neighborhoods

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

English

If f ≤ᶠ[𝓝 x] g, then for y near x we have f ≤ᶠ[𝓝 y] g.

Русский

Если f ≤ᶠ[ nhds x ] g, то при близких y к x имеем f ≤ᶠ[ nhds y ] g.

LaTeX

$$$(\\nN_x).EventuallyLE f g \\Rightarrow \\forall^* y \\in 𝓝 x,\\ f \\le^*_{𝓝 y} g.$$$

Lean4

@[simp]
theorem eventually_eventuallyLE_nhds [LE α] {f g : X → α} : (∀ᶠ y in 𝓝 x, f ≤ᶠ[𝓝 y] g) ↔ f ≤ᶠ[𝓝 x] g :=
  eventually_eventually_nhds

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

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

Разделы

Аффилиация

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