homeomorphCircle_apply — Mathlib

English

The canonical homeomorphism between AddCircle T and Circle acts on a point by sending its representative to the corresponding point on the unit circle via exponentiation.

Русский

Канонический гомеоморфизм между AddCircle T и Circle отправляет точку в соответствующую точку единичной окружности через экспоненциальное отображение.

LaTeX

$$$\\forall x \\ (x \\in AddCircle(T)):\\; (\\text{homeomorphCircle } h_T)(x) = toCircle(x)$.$$

Lean4

theorem homeomorphCircle_apply (hT : T ≠ 0) (x : AddCircle T) : homeomorphCircle hT x = toCircle x :=
  by
  cases x using QuotientAddGroup.induction_on
  rw [homeomorphCircle, Homeomorph.trans_apply, homeomorphAddCircle_apply_mk, homeomorphCircle'_apply_mk,
    toCircle_apply_mk]
  ring_nf

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