eventuallyLE_nhds — Mathlib

English

If f ≤ᶠ[𝓝 x] g then ∀ᶠ y ∈ 𝓝 x, f ≤ᶠ[𝓝 y] g.

Русский

Если f ≤ᶠ[ nhds x ] g, то ∀ᶠ y в nhds x выполняется f ≤ᶠ[ nhds y ] g.

LaTeX

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

Lean4

/-- If `f x ≤ g x` in a neighbourhood of `x`, then for `y` sufficiently close to `x` we have
`f x ≤ g x` in a neighbourhood of `y`. -/
theorem eventuallyLE_nhds [LE α] {f g : X → α} (h : f ≤ᶠ[𝓝 x] g) : ∀ᶠ y in 𝓝 x, f ≤ᶠ[𝓝 y] g :=
  h.eventually_nhds

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