Theorem: translationHomeo (src/MainTheorem.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x y : E
⊢ (fun x_1 => x_1 + -x) ((fun x_1 => x_1 + x) y) = y
Tactic:
simp
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x y : E
⊢ (fun x_1 => x_1 + x) ((fun x_1 => x_1 + -x) y) = y
Tactic:
simp
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
⊢ Continuous { toFun := fun x_1 => x_1 + x, invFun := fun x_1 => x_1 + -x, left_inv := ⋯, right_inv := ⋯ }.toFun
Tactic:
continuity
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
⊢ Continuous { toFun := fun x_1 => x_1 + x, invFun := fun x_1 => x_1 + -x, left_inv := ⋯, right_inv := ⋯ }.invFun
Tactic:
continuity
State after:
no goals