embedRealFun_strictMono — Mathlib

English

The map embedRealFun is strictly increasing: if x < y then embedRealFun(x) < embedRealFun(y).

Русский

Отображение embedRealFun строго возрастает: x < y ⇒ embedRealFun(x) < embedRealFun(y).

LaTeX

$$$\forall x

Lean4

theorem embedRealFun_strictMono : StrictMono (embedRealFun (M := M)) :=
  by
  intro x y h
  have hyz : 0 < y - x := sub_pos.mpr h
  have hy : y = y - x + x := (sub_add_cancel y x).symm
  apply lt_of_sub_pos
  rw [hy, embedRealFun_add, add_sub_cancel_right]
  obtain ⟨n, hn⟩ := Archimedean.arch 1 hyz
  have : (Rat.mk' 1 (n + 1) (by simp) (by simp) : ℝ) ∈ ratLt' (y - x) := by
    simpa using hn.trans_lt <| nsmul_lt_nsmul_left hyz (show n < n + 1 by simp)
  exact lt_csSup_of_lt (ratLt'_bddAbove (y - x)) this (by simp [← Rat.num_pos])

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