English
For any nonzero a in 𝕜 and any b, the affine map x ↦ a x + b is a homeomorphism of 𝕜 onto itself with inverse y ↦ (y − b)/a.
Русский
Для любых a ≠ 0 и b ∈ 𝕜 отображение x ↦ a x + b является гомеоморфизмом пространства 𝕜 в себя; обратное отображение задано как y ↦ (y − b)/a.
LaTeX
$$$f(x) = a x + b\quad (a \neq 0),\; f^{-1}(y) = \frac{y - b}{a},\; f \in \mathrm{Homeo}(\mathbb{k}, \mathbb{k}).$$$
Lean4
/-- The map `fun x => a * x + b`, as a homeomorphism from `𝕜` (a topological field) to itself,
when `a ≠ 0`.
-/
@[simps]
def affineHomeomorph (a b : 𝕜) (h : a ≠ 0) : 𝕜 ≃ₜ 𝕜
where
toFun x := a * x + b
invFun y := (y - b) / a
left_inv
x := by
simp only [add_sub_cancel_right]
exact mul_div_cancel_left₀ x h
right_inv y := by simp [mul_div_cancel₀ _ h]
