English
Let f: R →+* S be a ring hom between rings with certain order properties, and hf strictly monotone. Then mk x ≤ mk y is equivalent to the existence of q ∈ R with 0 < f(q) and f(q)|y| ≤ |x|.
Русский
Пусть f: R →+* S — кольцевой гомоморфизм между кольцами с заданными порядками, и hf строго монотонно. Тогда mk x ≤ mk y эквивалентно существованию q ∈ R с 0 < f(q) и f(q)|y| ≤ |x|.
LaTeX
$$$\forall x,y \in S,\ f:R\rightarrow^* S,\ hf:\,\text{StrictMono } f:\ mk x \le mk y \iff \exists q \in R,\ 0 < f q \land f q \cdot |y| \le |x|.$$$
Lean4
theorem mk_le_mk_iff_denselyOrdered [Ring S] [IsStrictOrderedRing S] [DenselyOrdered R] [Archimedean R] {x y : S}
(f : R →+* S) (hf : StrictMono f) : mk x ≤ mk y ↔ ∃ q : R, 0 < f q ∧ f q * |y| ≤ |x| :=
by
have H {q} : 0 < f q ↔ 0 < q := by simpa using hf.lt_iff_lt (a := 0)
constructor
· rintro ⟨(_ | n), hn⟩
· simp_all [exists_zero_lt]
· obtain ⟨q, hq₀, hq⟩ := exists_nsmul_lt_of_pos (one_pos (α := R)) (n + 1)
refine ⟨q, H.2 hq₀, le_of_mul_le_mul_left ?_ n.cast_add_one_pos⟩
simpa [← mul_assoc] using mul_le_mul (hf hq).le hn (abs_nonneg y) (by simp)
· rintro ⟨q, hq₀, hq⟩
have hq₀' := H.1 hq₀
obtain ⟨n, hn⟩ := exists_lt_nsmul hq₀' 1
refine ⟨n, le_of_mul_le_mul_left ?_ hq₀⟩
have h : 0 ≤ f (n • q) := by
rw [← f.map_zero]
exact hf.monotone (nsmul_nonneg hq₀'.le n)
simpa [mul_comm, mul_assoc] using mul_le_mul (hf hn).le hq (mul_nonneg hq₀.le (abs_nonneg y)) h
