English
If Γ₀ˣ is nontrivial and f: Γ₀ →*₀ ℝ≥0 is strictly monotone, then for any r > 0 there exists d with f(d) < r.
Русский
Если Γ₀ˣ не тривиально и f: Γ₀ →*₀ ℝ≥0 строго монотонна, то для любого r > 0 существует d, для которого f(d) < r.
LaTeX
$$$ [h : Nontrivial Γ₀^{\times}] \; {f : Γ₀ \to*_{0} ℝ≥0},\; (hf : StrictMono f) \Rightarrow (\forall r > 0, \exists d : Γ₀^{\times}, f(d) < r).$$$
Lean4
/-- If `Γ₀ˣ` is nontrivial and `f : Γ₀ →*₀ ℝ≥0` is strictly monotone, then for any positive
`r : ℝ≥0`, there exists `d : Γ₀ˣ` with `f d < r`. -/
theorem exists_lt_of_strictMono [h : Nontrivial Γ₀ˣ] {f : Γ₀ →*₀ ℝ≥0} (hf : StrictMono f) {r : ℝ≥0} (hr : 0 < r) :
∃ d : Γ₀ˣ, f d < r := by
obtain ⟨g, hg1⟩ := (nontrivial_iff_exists_ne (1 : Γ₀ˣ)).mp h
set u : Γ₀ˣ := if g < 1 then g else g⁻¹ with hu
have hfu : f u < 1 := by
rw [hu]
split_ifs with hu1
· rw [← map_one f]; exact hf hu1
· have hfg0 : f g ≠ 0 := fun h0 ↦ (Units.ne_zero g) ((map_eq_zero f).mp h0)
have hg1' : 1 < g := lt_of_le_of_ne (not_lt.mp hu1) hg1.symm
rw [Units.val_inv_eq_inv_val, map_inv₀, inv_lt_one_iff hfg0, ← map_one f]
exact hf hg1'
obtain ⟨n, hn⟩ := exists_pow_lt_of_lt_one hr hfu
use u ^ n
rwa [Units.val_pow_eq_pow_val, map_pow]
