20.2. Continuous maps🔗

If f is a function from X to Y, then to say "f is continuous", we write

Continuous[inst✝², inst✝¹] f : Prop#check Continuous f

Note that Continuous is unbundled, as opposed to how many types of functions are implemented in Mathlib, such as LinearMap.

example (hf : Continuous f) (hg : Continuous g) :
    Continuous (g ∘ f) :=
  hg.comp hf

For routine continuity goals, try fun_prop:

example : Continuous (fun p : X × Y => (p.2, p.1)) := byX:Type u_1Y:Type u_2Z:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace Yinst✝:TopologicalSpace Zs:Set Xx:Xf:X → Yg:Y → Z⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun p => (p.2, p.1)
  fun_propAll goals completed! 🐙

example : Continuous (fun x : ℝ => x^2 + 1) := byX:Type u_1Y:Type u_2Z:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace Yinst✝:TopologicalSpace Zs:Set Xx:Xf:X → Yg:Y → Z⊢ Continuous fun x => x ^ 2 + 1
  fun_propAll goals completed! 🐙

To state that a function is a homeomorphism, use IsHomeomorph.

IsHomeomorph.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Prop#check IsHomeomorph

The bundled versions of continous maps and homeomorphisms are ContinuousMap (which can be written using the notation C(X, Y)) and Homeomorph (which can be written as X ≃ₜ Y). These are useful when you want to put some structure on the collection of all continuous maps. For example, the vector space structure on C(ℝ, ℝ).

ContinuousMap.module#synth Module ℝ C(ℝ, ℝ)

The proof that a ContinuousMap is continuous is map_continuous. Given a function f and a proof it is continuous (hf : Continuous f), you can construct the corresponding ContinuousMap as ContinuousMap.mk f hf or simply ⟨f, hf⟩.

{ toFun := f, continuous_toFun := hf } : C(X, Y)#check (⟨f, hf⟩ : C(X, Y))

Homeomorph is a bit different as it bundles together both the function and its inverse, so there is more data contained here than just a function and a proof of IsHomeomorph. To upgrade an Equiv to a Homeomorph, use Equiv.toHomeomorph. This is the prefered way of constructing homeomorphisms. Given a proof of (hf : IsHomeomorph f), you can construct the corresponding Homeomorph as hf.homeomorph but this should only be done when you don't have a constructive way of defining the inverse of f. To go from a Homeomorph to a ContinuousMap, use map_continuous.

Some other function properties are IsOpenMap, IsClosedMap, Topology.IsEmbedding, Topology.IsOpenEmbedding, Topology.IsClosedEmbedding, and Topology.IsQuotientMap.