English
A set-theoretic relation between inverses on a structured set with special elements demonstrates symmetry of inverse operations on a bounded interval.
Русский
Отношение между обратными операциями на заданном множестве демонстрирует симметричность обратных операций на ограниченном интервале.
LaTeX
$$$$ \text{Set.InvOn}\bigl( f, g, \{x : \mathbb{R}_{\ge 0} \mid x < 1\}, \{x : \mathbb{R}_{\ge 0} \mid x < 1\} \bigr) $$$$
Lean4
theorem one_sub_one_add_inv :
Set.InvOn (fun x ↦ 1 - (1 + x)⁻¹) (fun x ↦ x * (1 - x)⁻¹) {x : ℝ≥0 | x < 1} {x : ℝ≥0 | x < 1} :=
by
have : (fun x : ℝ≥0 ↦ x * (1 + x)⁻¹) = fun x ↦ 1 - (1 + x)⁻¹ :=
by
ext x : 1
simp [field, mul_tsub]
rw [← this]
constructor <;> intro x (hx : x < 1)
· have : 0 < 1 - x := tsub_pos_of_lt hx
simp [field, tsub_add_cancel_of_le hx.le]
· simp [mul_assoc, ← mul_inv, mul_tsub]
field_simp
simp
