English
Similarly, for a strictly monotone f: Γ₀ →*₀ ℝ≥0, there exists d with f(d) < r for r > 0.
Русский
А именно, для строго монотонной f: Γ₀ →*₀ ℝ≥0 существует d, где f(d) < r при r > 0.
LaTeX
$$$ [h : Nontrivial Γ₀^{\times}] {f : Γ₀ \to*_{0} ℝ≥0} (hf : StrictMono f) {r : \mathbb{R}} (hr : 0 < r) \Rightarrow \exists d : Γ₀^{\times}, (f d) < r.$$$
Lean4
/-- If `Γ₀ˣ` is nontrivial and `f : Γ₀ →*₀ ℝ≥0` is strictly monotone, then for any positive
real `r`, there exists `d : Γ₀ˣ` with `f d < r`. -/
theorem exists_lt_of_strictMono [h : Nontrivial Γ₀ˣ] {f : Γ₀ →*₀ ℝ≥0} (hf : StrictMono f) {r : ℝ} (hr : 0 < r) :
∃ d : Γ₀ˣ, (f d : ℝ) < r := by
set s : NNReal := ⟨r, le_of_lt hr⟩
have hs : 0 < s := hr
exact NNReal.exists_lt_of_strictMono hf hs
