eventually_mabs_div_lt — Mathlib

English

For any a and any ε > 1, the set { x : |x / a|_m < ε } belongs to the neighborhood 𝓝(a); i.e., the condition holds eventually near a.

Русский

Для любого a и ε>1 множество { x : |x/a|_m < ε } принадлежит окрестностям a; услоево eventually относительно 𝓝(a).

LaTeX

$$$$\forall a\in\alpha:\ \forall \varepsilon>1:\ {x\in\alpha : |x/a|_{m} < \varepsilon} \in 𝒩(a). $$$$

Lean4

@[to_additive]
theorem eventually_mabs_div_lt (a : α) {ε : α} (hε : 1 < ε) : ∀ᶠ x in 𝓝 a, |x / a|ₘ < ε :=
  (nhds_eq_iInf_mabs_div a).symm ▸
    mem_iInf_of_mem ε (mem_iInf_of_mem hε <| by simp only [mabs_div_comm, mem_principal_self])

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