G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hbot : S ≠ ⊥
H : ¬∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a
ε : G
ε0 : ε > 0
⊢ ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hbot : S ≠ ⊥
H : ¬∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a
⊢ Dense ↑S
refine S.dense_of_not_isolated_zero fun ε ε0 => ?_
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hbot : S ≠ ⊥
ε : G
ε0 : ε > 0
H : ∀ (g : G), g ∈ S → ¬g ∈ Ioo 0 ε
⊢ ∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hbot : S ≠ ⊥
H : ¬∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a
ε : G
ε0 : ε > 0
⊢ ∃ g, g ∈ S ∧ g ∈ Ioo 0 ε
contrapose! H
no goals
G : Type u_1
inst✝³ : LinearOrderedAddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : Archimedean G
S : AddSubgroup G
hbot : S ≠ ⊥
ε : G
ε0 : ε > 0
H : ∀ (g : G), g ∈ S → ¬g ∈ Ioo 0 ε
⊢ ∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a
exact exists_isLeast_pos hbot ε0 (disjoint_left.2 H)