Cartesian coordinates as a homeomorphism

Definition

LeanFormalizations_PachDeZeeuw_ChartBridge

by mysticflounder · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

topology

This defines the coordinate homeomorphism from the two-dimensional real Euclidean space to the Cartesian product of two real lines.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_LeanFormalizations_PachDeZeeuw_Bezout
import Mathlib

set_option autoImplicit true

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/


set_option linter.style.longLine false

namespace PachDeZeeuw.Algebraic

open scoped Topology


noncomputable def chartEquiv : EuclideanSpace ℝ (Fin 2) ≃ₜ ℝ × ℝ :=
  (EuclideanSpace.equiv (Fin 2) ℝ).toHomeomorph.trans Homeomorph.finTwoArrow

scoped notation "E" => chartEquiv


end PachDeZeeuw.Algebraic

View graph