homeomorphCircle — Mathlib

English

For every nonzero T, the additive circle AddCircle T is topologically equivalent to the circle Circle; there exists a canonical homeomorphism between them.

Русский

Для каждого ненулевого T аддитивный круг AddCircle T гомеоморфен окружности Circle; существует канонический гомеоморфизм между ними.

LaTeX

$$$T \\neq 0 \\implies AddCircle(T) \\simeq_{\\mathrm{top}} Circle$$$

Lean4

/-- The homeomorphism between `AddCircle` and `Circle`. -/
noncomputable def homeomorphCircle (hT : T ≠ 0) : AddCircle T ≃ₜ Circle :=
  (homeomorphAddCircle T (2 * π) hT (by positivity)).trans homeomorphCircle'

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