English
The map x ↦ x^{-1} is strictly decreasing on the positive region Ioi 0 of EReal.
Русский
Обратная функция x ↦ x^{-1} строго убывает на положительной части EReal (Ioi 0).
LaTeX
$$SStrictAntiOn(x \mapsto x^{-1}) \; (Ioi\ 0)$$
Lean4
theorem inv_strictAntiOn : StrictAntiOn (fun (x : EReal) => x⁻¹) (Ioi 0) :=
by
intro a a_0 b b_0 a_b
simp only [mem_Ioi] at *
lift a to ℝ using ⟨ne_top_of_lt a_b, ne_bot_of_gt a_0⟩
match b with
| ⊤ => exact inv_top ▸ inv_pos_of_pos_ne_top a_0 (coe_ne_top a)
| ⊥ => exact (not_lt_bot b_0).rec
| (b : ℝ) =>
rw [← coe_inv a, ← coe_inv b, EReal.coe_lt_coe_iff]
exact _root_.inv_strictAntiOn (EReal.coe_pos.1 a_0) (EReal.coe_pos.1 b_0) (EReal.coe_lt_coe_iff.1 a_b)
