Mathoverflow 235893

Reference: mathoverflow/235893 asked by user Willie Wong

def Mathoverflow235893.IsConnectedMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Prop

For topological spaces $X$ and $Y$ we say a function $f : X → Y$ is connected is it sends connected sets to connected sets.

Equations

• Mathoverflow235893.IsConnectedMap f = ∀ ⦃s : Set X⦄, IsConnected s → IsConnected (f '' s)

theorem Mathoverflow235893.Continuous.isConnectedMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) : IsConnectedMap f

By a standard result, every continuous map is connected

theorem Mathoverflow235893.isConnected_iff_ordConnected_and_nonempty {s : Set ℝ} : IsConnected s ↔ s.OrdConnected ∧ s.Nonempty

A set in $\mathbb{R}$ is connected if and only if it is order-connected and non-empty.

theorem Mathoverflow235893.isConnectedMap_symm_of_R (f : ℝ ≃ ℝ) (hf : IsConnectedMap ⇑f) : IsConnectedMap ⇑f.symm

If $f : \mathbb{R} \to \mathbb{R}$ is a connected bijection, then its inverse is also a connected bijection.

theorem Mathoverflow235893.isConnectedMap_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : IsConnectedMap f) (hg : IsConnectedMap g) : IsConnectedMap (g ∘ f)

The composition of two connected maps is a connected map.

theorem Mathoverflow235893.isConnectedMap_homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsConnectedMap ⇑h

A homeomorphism is a connected map.

theorem Mathoverflow235893.isConnectedMap_symm_of_E1 (f : EuclideanSpace ℝ (Fin 1) ≃ EuclideanSpace ℝ (Fin 1)) (hf : IsConnectedMap ⇑f) : IsConnectedMap ⇑f.symm

If $f : \mathbb{R}^1 \to \mathbb{R}^1$ is a connected bijection, then its inverse is also a connected bijection.

theorem Mathoverflow235893.mathoverflow_235893 : True ↔ ∀ n > 1, ∀ (f : EuclideanSpace ℝ (Fin n) ≃ EuclideanSpace ℝ (Fin n)), IsConnectedMap ⇑f → IsConnectedMap ⇑f.symm

Assume for $n>1$, $f:\mathbb{R}^n\to\mathbb{R}^n$ is a bijection, where $\mathbb{R}^n$ is equipped with the standard topology. Does the connectedness of (the induced power set map) $f$ imply that of $f^{-1}$?

theorem Mathoverflow235893.mathoverflow_260589 : ∃ (f : ℝ ≃ EuclideanSpace ℝ (Fin 2)), IsConnectedMap ⇑f ∧ ¬IsConnectedMap ⇑f.symm

There exists a connected bijection ℝ → ℝ^2 where the inverse is not connected, proven in mathoverflow/260589 by user Gro-Tsen.