/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilMathoverflow 235893
Reference: mathoverflow/235893 asked by user Willie Wong
open scoped EuclideanGeometrynamespace Mathoverflow235893variable (n : ℕ)For topological spaces $X$ and $Y$ we say a function $f : X → Y$ is connected is it sends connected sets to connected sets.
def IsConnectedMap {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Prop :=
∀ ⦃s : Set X⦄, IsConnected s → IsConnected (f '' s)By a standard result, every continuous map is connected
@[category test, AMS 54]
theorem Continuous.isConnectedMap {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
{f : X → Y} (hf : Continuous f) : IsConnectedMap f :=
fun _ h ↦ IsConnected.image h f (Continuous.continuousOn hf)A set in $\mathbb{R}$ is connected if and only if it is order-connected and non-empty.
@[category test, AMS 54]
lemma isConnected_iff_ordConnected_and_nonempty {s : Set ℝ} :
IsConnected s ↔ s.OrdConnected ∧ s.Nonempty := s:Set ℝ⊢ IsConnected s ↔ s.OrdConnected ∧ s.Nonempty
/-
We prove this by combining the facts that connected sets in $\mathbb{R}$ are exactly the order-connected sets, and that connected sets are by definition non-empty.
-/
s:Set ℝ⊢ IsConnected s → s.OrdConnected ∧ s.Nonemptys:Set ℝ⊢ s.OrdConnected ∧ s.Nonempty → IsConnected s
s:Set ℝ⊢ IsConnected s → s.OrdConnected ∧ s.Nonempty s:Set ℝh1:s.Nonemptyh2:IsPreconnected s⊢ s.OrdConnected ∧ s.Nonempty
All goals completed! 🐙
s:Set ℝ⊢ s.OrdConnected ∧ s.Nonempty → IsConnected s s:Set ℝh1:s.OrdConnectedh2:s.Nonempty⊢ IsConnected s
All goals completed! 🐙If $f : \mathbb{R} \to \mathbb{R}$ is a connected bijection, then its inverse is also a connected bijection.
f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonemptya:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c)hI1:IsConnected (Set.Icc a b)hI2:IsConnected (Set.Icc b c)hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a bh_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b ch_gt:max (f a) (f c) < f by:ℝ := max (f a) (f c)hy1:y ∈ Set.uIcc (f a) (f b)hy2:y ∈ Set.uIcc (f b) (f c)x1:ℝhx1:x1 ∈ Set.Icc a bhfx1:f x1 = yx2:ℝhx2:x2 ∈ Set.Icc b chfx2:f x2 = yh_eq:x1 = x2h_eq_b:x1 = bthis:f b = max (f a) (f c)⊢ False
All goals completed! 🐙The composition of two connected maps is a connected map.
X:Type u_1Y:Type u_2Z:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace Yinst✝:TopologicalSpace Zf:X → Yg:Y → Zhf:IsConnectedMap fhg:IsConnectedMap gs:Set Xhs:IsConnected s⊢ IsConnected (g '' f '' s)
All goals completed! 🐙A homeomorphism is a connected map.
@[category test, AMS 54]
lemma isConnectedMap_homeomorph {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
(h : X ≃ₜ Y) : IsConnectedMap h := X:Type u_1Y:Type u_2inst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yh:X ≃ₜ Y⊢ IsConnectedMap ⇑h
/-
We prove this by noting that a homeomorphism is continuous, and continuous maps preserve connectedness.
-/
X:Type u_1Y:Type u_2inst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yh:X ≃ₜ Ys:Set Xhs:IsConnected s⊢ IsConnected (⇑h '' s)
All goals completed! 🐙If $f : \mathbb{R}^1 \to \mathbb{R}^1$ is a connected bijection, then its inverse is also a connected bijection.
f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑fh:ℝ^1 ≃ₜ ℝ := (EuclideanSpace.equiv (Fin 1) ℝ).toHomeomorph.trans (Homeomorph.funUnique (Fin 1) ℝ)g:ℝ ≃ ℝ := h.symm.trans (f.trans h.toEquiv)hg_conn:IsConnectedMap ⇑ghg_symm_conn:IsConnectedMap ⇑g.symmhf_eq:⇑f.symm = ⇑h.symm ∘ ⇑g.symm ∘ ⇑h⊢ IsConnectedMap (⇑h.symm ∘ ⇑g.symm ∘ ⇑h)
f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑fh:ℝ^1 ≃ₜ ℝ := (EuclideanSpace.equiv (Fin 1) ℝ).toHomeomorph.trans (Homeomorph.funUnique (Fin 1) ℝ)g:ℝ ≃ ℝ := h.symm.trans (f.trans h.toEquiv)hg_conn:IsConnectedMap ⇑ghg_symm_conn:IsConnectedMap ⇑g.symmhf_eq:⇑f.symm = ⇑h.symm ∘ ⇑g.symm ∘ ⇑hh1:IsConnectedMap ⇑h⊢ IsConnectedMap (⇑h.symm ∘ ⇑g.symm ∘ ⇑h)
f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑fh:ℝ^1 ≃ₜ ℝ := (EuclideanSpace.equiv (Fin 1) ℝ).toHomeomorph.trans (Homeomorph.funUnique (Fin 1) ℝ)g:ℝ ≃ ℝ := h.symm.trans (f.trans h.toEquiv)hg_conn:IsConnectedMap ⇑ghg_symm_conn:IsConnectedMap ⇑g.symmhf_eq:⇑f.symm = ⇑h.symm ∘ ⇑g.symm ∘ ⇑hh1:IsConnectedMap ⇑hh2:IsConnectedMap ⇑h.symm⊢ IsConnectedMap (⇑h.symm ∘ ⇑g.symm ∘ ⇑h)
f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑fh:ℝ^1 ≃ₜ ℝ := (EuclideanSpace.equiv (Fin 1) ℝ).toHomeomorph.trans (Homeomorph.funUnique (Fin 1) ℝ)g:ℝ ≃ ℝ := h.symm.trans (f.trans h.toEquiv)hg_conn:IsConnectedMap ⇑ghg_symm_conn:IsConnectedMap ⇑g.symmhf_eq:⇑f.symm = ⇑h.symm ∘ ⇑g.symm ∘ ⇑hh1:IsConnectedMap ⇑hh2:IsConnectedMap ⇑h.symm⊢ IsConnectedMap (⇑h.symm ∘ ⇑g.symm ∘ ⇑h)
All goals completed! 🐙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}$?
@[category research open, AMS 26 54]
theorem mathoverflow_235893 :
answer(sorry) ↔ ∀ n > 1, ∀ (f : ℝ^n ≃ ℝ^n), IsConnectedMap f → IsConnectedMap f.symm := ⊢ True ↔ ∀ n > 1, ∀ (f : ℝ^n ≃ ℝ^n), IsConnectedMap ⇑f → IsConnectedMap ⇑f.symm
All goals completed! 🐙There exists a connected bijection ℝ → ℝ^2 where the inverse is not connected, proven in mathoverflow/260589 by user Gro-Tsen.
@[category research solved, AMS 26 54]
theorem mathoverflow_260589 :
∃ f : ℝ ≃ ℝ^2, IsConnectedMap f ∧ ¬ IsConnectedMap f.symm := ⊢ ∃ f, IsConnectedMap ⇑f ∧ ¬IsConnectedMap ⇑f.symm
All goals completed! 🐙-- TODO: Add remarks from the mathoverflow post
end Mathoverflow235893