Theorems · Theorem · order theory

AddSubgroup.exists_isLeast_pos

∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G]
  {H : AddSubgroup G}, H ≠ ⊥ → ∀ {a : G}, 0 < a → Disjoint (↑H) (Set.Ioo 0 a) → ∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b

If a nontrivial additive subgroup of a linear ordered additive commutative group is disjoint with the interval Set.Ioo 0 a for some positive a, then the set of positive elements of this group admits the least element.

Defined in

Mathlib.GroupTheory.Archimedean

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidArchimedean