Theorems · Theorem · order theory

LinearOrderedCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete

∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [Nontrivial G] {g : G},
  ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Defined in

Mathlib.GroupTheory.ArchimedeanDensely

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommGroupLinearOrderIsOrderedMonoidNontrivial