Order-connected subgroups and archimedean classes

[UPSTREAM] candidate for Mathlib/Algebra/Order/Archimedean/Class.lean. A subgroup of a linearly ordered abelian group is order-connected, a convex subgroup, as soon as it contains every element between zero and one of its elements. The subgroups that upper sets of archimedean classes cut out, among them ballAddSubgroup and closedBallAddSubgroup, are order-connected.

theorem AddSubgroup.ordConnected_of_Icc_zero_subset {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : AddSubgroup G} (h : ∀ b ∈ H, Set.Icc 0 b ⊆ ↑H) : (↑H).OrdConnected

A subgroup is order-connected when it contains every element between zero and one of its elements.

theorem AddSubgroup.exists_pos_mem_of_ne_bot {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : AddSubgroup G} (h : H ≠ ⊥) : ∃ a ∈ H, 0 < a

A nontrivial subgroup has a positive element.

theorem ArchimedeanClass.ordConnected_addSubgroup {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (s : UpperSet (ArchimedeanClass G)) : (↑(addSubgroup s)).OrdConnected

The subgroup an upper set of archimedean classes cuts out is order-connected.

theorem ArchimedeanClass.ordConnected_ballAddSubgroup {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (c : ArchimedeanClass G) : (↑c.ballAddSubgroup).OrdConnected

theorem ArchimedeanClass.ordConnected_closedBallAddSubgroup {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (c : ArchimedeanClass G) : (↑c.closedBallAddSubgroup).OrdConnected