homeomorphAddCircle_symm_apply_mk

English

The inverse of the circle homeomorphism sends x to x(q⁻¹p) in the opposite circle.

Русский

Обратное гомеоморфизма круга отправляет x в x(q⁻¹p) в противоположной окружности.

LaTeX

$$$(\mathrm{homeomorphAddCircle}(p,q)(hp,hq))^{-1}(x) = x(q^{-1}p)$$$

Lean4

@[simp]
theorem homeomorphAddCircle_symm_apply_mk (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) :
    (homeomorphAddCircle p q hp hq).symm (x : 𝕜) = (x * (q⁻¹ * p) : 𝕜) :=
  rfl

Похожие утверждения