eventually_nhdsGT_zero_mul_left — Mathlib

English

If 0 < x and a property holds eventually near 0+ for ε, then it holds eventually for x·ε.

Русский

Если 0 < x и для ε рядом с 0 слева выполняется свойство, то аналогично свойство выполняется и для x·ε.

LaTeX

$$If hx: 0 < x and h: ∀ᶠ ε ∈ 𝓝[>] 0, p ε, then ∀ᶠ ε ∈ 𝓝[>] 0, p (x ε).$$

Lean4

theorem eventually_nhdsGT_zero_mul_left {x : 𝕜} (hx : 0 < x) {p : 𝕜 → Prop} (h : ∀ᶠ ε in 𝓝[>] 0, p ε) :
    ∀ᶠ ε in 𝓝[>] 0, p (x * ε) := by
  rw [← comap_mulLeft_nhdsGT_zero hx]
  exact h.comap fun ε => x * ε

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