Theorems · Theorem · order theory

ArchimedeanClass.mk_nonneg_of_le_of_le_of_archimedean

∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {S : Type u_3}
  [inst_3 : LinearOrder S] [inst_4 : CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+*o R) {x : R}
  {r s : S}, f r ≤ x → x ≤ f s → 0 ≤ ArchimedeanClass.mk x

Defined in

Mathlib.Algebra.Order.Ring.Archimedean

Cited by

3 results in Mathlib

Foundations

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

Assumes

LinearOrderCommRingIsStrictOrderedRingLinearOrderCommRingIsStrictOrderedRingArchimedean