Theorems · Theorem · field theory

ConditionallyCompleteLinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self

∀ {α : Type u_2} {β : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α},
  0 < a →
    ∀
      b <
        ConditionallyCompleteLinearOrderedField.inducedMap α β a *
          ConditionallyCompleteLinearOrderedField.inducedMap α β a,
      ∃ c ∈ LinearOrderedField.cutMap β (a * a), b < c

Preparatory lemma for inducedOrderRingHom.

Defined in

Mathlib.Algebra.Order.CompleteField

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRingFieldConditionallyCompleteLinearOrderIsStrictOrderedRingArchimedean