Theorems · Theorem · order theory

Subgroup.exists_isLeast_one_lt

∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {H : Subgroup G},
  H ≠ ⊥ → ∀ {a : G}, 1 < a → Disjoint (↑H) (Set.Ioo 1 a) → ∃ b, IsLeast {g | g ∈ H ∧ 1 < g} b

If a nontrivial subgroup of a linear ordered commutative group is disjoint with the interval Set.Ioo 1 a for some 1 < a, then the set of elements greater than 1 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

CommGroupLinearOrderIsOrderedMonoidMulArchimedean