le_inducedMap_mul_self_of_mem_cutMap

English

If a > 0 and b belongs to the cut of a^2 in β, then b is bounded above by the square of the induced map a; i.e., b ≤ (inducedMap α β a)^2.

Русский

Пусть a > 0 и b принадлежит множеству-cut β(a^2). Тогда b не превосходит квадрата индуцированного отображения a: b ≤ (inducedMap α β a)^2.

LaTeX

$$$ a > 0 \wedge b \in cutMap \beta (a^2) \Rightarrow b \le (\mathrm{inducedMap} \alpha \beta a)^2 $$$

Lean4

/-- Preparatory lemma for `inducedOrderRingHom`. -/
theorem le_inducedMap_mul_self_of_mem_cutMap (ha : 0 < a) (b : β) (hb : b ∈ cutMap β (a * a)) :
    b ≤ inducedMap α β a * inducedMap α β a := by
  obtain ⟨q, hb, rfl⟩ := hb
  obtain ⟨q', hq', hqq', hqa⟩ := exists_rat_pow_btwn two_ne_zero hb (mul_self_pos.2 ha.ne')
  trans (q' : β) ^ 2
  · exact mod_cast hqq'.le
  · rw [pow_two] at hqa ⊢
    exact
      mul_self_le_mul_self (mod_cast hq'.le)
        (le_csSup (cutMap_bddAbove β a) <| coe_mem_cutMap_iff.2 <| lt_of_mul_self_lt_mul_self₀ ha.le hqa)

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