Theorems · Theorem · order theory

AddSubgroup.dense_of_not_isolated_zero

∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [Archimedean G] (S : AddSubgroup G), (∀ ε > 0, ∃ g ∈ S, g ∈ Set.Ioo 0 ε) → Dense ↑S

An additive subgroup of an archimedean linear ordered additive commutative group with order topology is dense provided that for all positive ε there exists a positive element of the subgroup that is less than ε.

Defined in

Mathlib.Topology.Algebra.Order.Archimedean

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidTopologicalSpaceOrderTopologyArchimedean