isHomeomorphicTrivialFiberBundle_im

English

The imaginary coordinate projection also yields a trivial real fiber bundle structure on ℂ.

Русский

Проекция мнимая координата также задаёт тривиальную структуру волокна над ℝ на ℂ.

LaTeX

$$ℂ ≅ℝ × ℝ via z ↦ (Im z, Re z).$$

Lean4

/-- `Complex.im` turns `ℂ` into a trivial topological fiber bundle over `ℝ`. -/
theorem isHomeomorphicTrivialFiberBundle_im : IsHomeomorphicTrivialFiberBundle ℝ im :=
  ⟨equivRealProdCLM.toHomeomorph.trans (Homeomorph.prodComm ℝ ℝ), fun _ => rfl⟩

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