inducedOrderRingHom — Mathlib

English

If a > 0 and b < (inducedMap α β a)^2, then there exists c ∈ cutMap β (a^2) with b < c.

Русский

Пусть a > 0 и b меньше чем (inducedMap α β a)^2; тогда существует c ∈ cutMap β (a^2) такое, что b < c.

LaTeX

$$$ a > 0 \wedge b < (\mathrm{inducedMap} \alpha \beta a)^2 \Rightarrow \exists c \in cutMap \beta (a^2),\; b < c $$$

Lean4

/-- `inducedMap` as an `OrderRingHom`. -/
@[simps!]
def inducedOrderRingHom : α →+*o β :=
  {
    AddMonoidHom.mkRingHomOfMulSelfOfTwoNeZero (inducedAddHom α β)
      (by
        suffices ∀ x, 0 < x → inducedAddHom α β (x * x) = inducedAddHom α β x * inducedAddHom α β x
          by
          intro x
          obtain h | rfl | h := lt_trichotomy x 0
          · convert this (-x) (neg_pos.2 h) using 1
            · rw [neg_mul, mul_neg, neg_neg]
            · simp_rw [AddMonoidHom.map_neg, neg_mul, mul_neg, neg_neg]
          · simp only [mul_zero, AddMonoidHom.map_zero]
          · exact this x h
        refine fun x hx => csSup_eq_of_forall_le_of_forall_lt_exists_gt (cutMap_nonempty β _) ?_ ?_
        · exact le_inducedMap_mul_self_of_mem_cutMap hx
        · exact exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self hx)
      (two_ne_zero) (inducedMap_one _ _) with
    monotone' := inducedMap_mono _ _ }

Похожие утверждения