Theorems · Theorem · general topology

eventually_mabs_div_lt

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CommGroup α] [inst_2 : LinearOrder α] [IsOrderedMonoid α]
  [OrderTopology α] (a : α) {ε : α}, 1 < ε → ∀ᶠ (x : α) in nhds a, |x / a|ₘ < ε

Defined in

Mathlib.Topology.Order.LeftRightNhds

Cited by

0 results in Mathlib

Foundations

Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceCommGroupLinearOrderIsOrderedMonoidOrderTopology