Formalising Mathematics with Lean

3.4. Continuity🔗

Definition 3.9🔗

Let X and Y be two topological spaces and f : X \to Y a function between them. Then f is continuous at a point x_0 \in X if for each neighbourhood V of f(x_0) in Y, we have that f^{-1}(V) is a neighbourhood of x_0 in X. We will say that f is continuous on X if it is continuous at every point.

Proposition 3.9 (Characterisation of continuous functions)🔗

Let X and Y be two topological spaces and f : X \to Y a function between them. Then f is continuous if and only if for each open V \subseteq Y, we have that f^{-1}(V) is open in X.

Proof. Let us see both implications separately.

example (X Y : Type) [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : (∀ x : X, ∀ V : Set Y, Neighbourhood V (f x) → Neighbourhood (f ⁻¹' V) x) ↔ ∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V) := X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Y⊢ (∀ (x : X) (V : Set Y), Neighbourhood V (f x) → Neighbourhood (f ⁻¹' V) x) ↔ ∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V) X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Y⊢ (∀ (x : X) (V : Set Y), Neighbourhood V (f x) → Neighbourhood (f ⁻¹' V) x) → ∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Y⊢ (∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)) → ∀ (x : X) (V : Set Y), Neighbourhood V (f x) → Neighbourhood (f ⁻¹' V) x; all_goals X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)⊢ ∀ (x : X) (V : Set Y), Neighbourhood V (f x) → Neighbourhood (f ⁻¹' V) x

(\implies) Let f : X \to Y be continuous and let V \subseteq Y be an open set. We want to see that f^{-1}(V) is open. To do so, it suffices to see that it is a neighbourhood of all of its points (Prop. 3.1).

Let x \in f^{-1}(V). Then V is a neighbourhood of f(x), since V is an open set with f(x) \in V. Hence, by the definition of continuity, f^{-1}(V) is a neighbourhood of x.

X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (x : X) (V : Set Y), Neighbourhood V (f x) → Neighbourhood (f ⁻¹' V) x⊢ ∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V) intro V X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (x : X) (V : Set Y), Neighbourhood V (f x) → Neighbourhood (f ⁻¹' V) xV:Set YhVopen:IsOpen V⊢ IsOpen (f ⁻¹' V) X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (x : X) (V : Set Y), Neighbourhood V (f x) → Neighbourhood (f ⁻¹' V) xV:Set YhVopen:IsOpen V⊢ ∀ x ∈ f ⁻¹' V, Neighbourhood (f ⁻¹' V) x intro x X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (x : X) (V : Set Y), Neighbourhood V (f x) → Neighbourhood (f ⁻¹' V) xV:Set YhVopen:IsOpen Vx:Xhx:x ∈ f ⁻¹' V⊢ Neighbourhood (f ⁻¹' V) x exact h x V (X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (x : X) (V : Set Y), Neighbourhood V (f x) → Neighbourhood (f ⁻¹' V) xV:Set YhVopen:IsOpen Vx:Xhx:x ∈ f ⁻¹' V⊢ Neighbourhood V (f x) X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (x : X) (V : Set Y), Neighbourhood V (f x) → Neighbourhood (f ⁻¹' V) xV:Set YhVopen:IsOpen Vx:Xhx:x ∈ f ⁻¹' V⊢ V ⊆ V ∧ OpenNeighbourhood V (f x); X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (x : X) (V : Set Y), Neighbourhood V (f x) → Neighbourhood (f ⁻¹' V) xV:Set YhVopen:IsOpen Vx:Xhx:x ∈ f ⁻¹' V⊢ OpenNeighbourhood V (f x); All goals completed! 🐙)

(\impliedby) Let now x \in X and let V \subseteq Y be a neighbourhood of f(x) in Y. We want to see that f^{-1}(V) is a neighbourhood of x in X.

There exists an open neighbourhood U\subseteq V of f(x) in Y. Then x \in f^{-1}(U)\subseteq f^{-1}(V), and it is open, by hypothesis. Therefore f^{-1}(V) is a neighbourhood of x.

X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)⊢ ∀ (x : X) (V : Set Y), Neighbourhood V (f x) → Neighbourhood (f ⁻¹' V) x intro x X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)x:XV:Set Y⊢ Neighbourhood V (f x) → Neighbourhood (f ⁻¹' V) x X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)x:XV:Set YhV:Neighbourhood V (f x)⊢ Neighbourhood (f ⁻¹' V) x X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)x:XV:Set YU:Set YhUV:U ⊆ VhU:OpenNeighbourhood U (f x)⊢ Neighbourhood (f ⁻¹' V) x X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)x:XV:Set YU:Set YhUV:U ⊆ VhUx:f x ∈ UhUopen:IsOpen U⊢ Neighbourhood (f ⁻¹' V) x X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)x:XV:Set YU:Set YhUV:U ⊆ VhUx:f x ∈ UhUopen:IsOpen U⊢ f ⁻¹' U ⊆ f ⁻¹' V ∧ OpenNeighbourhood (f ⁻¹' U) x X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)x:XV:Set YU:Set YhUV:U ⊆ VhUx:f x ∈ UhUopen:IsOpen U⊢ f ⁻¹' U ⊆ f ⁻¹' VX:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)x:XV:Set YU:Set YhUV:U ⊆ VhUx:f x ∈ UhUopen:IsOpen U⊢ OpenNeighbourhood (f ⁻¹' U) x X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)x:XV:Set YU:Set YhUV:U ⊆ VhUx:f x ∈ UhUopen:IsOpen U⊢ f ⁻¹' U ⊆ f ⁻¹' V intro u X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)x:XV:Set YU:Set YhUV:U ⊆ VhUx:f x ∈ UhUopen:IsOpen Uu:Xhu:u ∈ f ⁻¹' U⊢ u ∈ f ⁻¹' V X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)x:XV:Set YU:Set YhUV:U ⊆ VhUx:f x ∈ UhUopen:IsOpen Uu:Xhu:u ∈ f ⁻¹' U⊢ f u ∈ U All goals completed! 🐙 X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)x:XV:Set YU:Set YhUV:U ⊆ VhUx:f x ∈ UhUopen:IsOpen U⊢ OpenNeighbourhood (f ⁻¹' U) x X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)x:XV:Set YU:Set YhUV:U ⊆ VhUx:f x ∈ UhUopen:IsOpen U⊢ x ∈ f ⁻¹' UX:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)x:XV:Set YU:Set YhUV:U ⊆ VhUx:f x ∈ UhUopen:IsOpen U⊢ IsOpen (f ⁻¹' U) X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)x:XV:Set YU:Set YhUV:U ⊆ VhUx:f x ∈ UhUopen:IsOpen U⊢ x ∈ f ⁻¹' U All goals completed! 🐙 X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)x:XV:Set YU:Set YhUV:U ⊆ VhUx:f x ∈ UhUopen:IsOpen U⊢ IsOpen (f ⁻¹' U) All goals completed! 🐙

∎

Since both definitions are equivalent, Mathlib uses the second one to define continuous functions, and in general we will use this definition.

structure Continuous (f : X → Y) : Prop where isOpen_preimage : ∀ s, IsOpen s → IsOpen (f ⁻¹' s)

We will use continuous_def to rewrite Continuous f into this definition whenever we need it.

Example 3.13🔗

Let f : (X, \mathcal{T}_{disc}) \to (Y, \mathcal{T}) be a function where the domain has the discrete topology (Ex. 3.1). Then f is continuous.

If we take any open set of Y, its preimage will be trivially open in the discrete topology, since every set is.

lemma continuous_from_discrete {X Y : Type} [T : TopologicalSpace X] [TopologicalSpace Y] (h : T = DiscreteTopo X) (f : X → Y) : Continuous f := X:TypeY:TypeT:TopologicalSpace Xinst✝:TopologicalSpace Yh:T = DiscreteTopo Xf:X → Y⊢ Continuous f X:TypeY:TypeT:TopologicalSpace Xinst✝:TopologicalSpace Yh:T = DiscreteTopo Xf:X → Y⊢ ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s) intro U X:TypeY:TypeT:TopologicalSpace Xinst✝:TopologicalSpace Yh:T = DiscreteTopo Xf:X → YU:Set Ya✝:IsOpen U⊢ IsOpen (f ⁻¹' U) -- aquí lo que hago es que le digo -- que estoy trabajando con la discreta X:TypeY:TypeT:TopologicalSpace Xinst✝:TopologicalSpace Yh:T = DiscreteTopo Xf:X → YU:Set Ya✝:IsOpen U⊢ IsOpen (f ⁻¹' U) -- (Aunque parezca que no hago nada) All goals completed! 🐙

Example 3.14🔗

Let f : (X, \mathcal{T}) \to (Y, \mathcal{T}_{trivial}) be a function where the codomain has the trivial topology (Ex. 3.2). Then f is continuous.

Since the only possible open sets to take in Y are Y itself and the empty set, their preimages will be, respectively, X and the empty set, which are open.

lemma continuous_to_trivial {X Y : Type} [TopologicalSpace X] [T : TopologicalSpace Y] (h : T = TrivialTopology Y) (f : X → Y) : Continuous f := X:TypeY:Typeinst✝:TopologicalSpace XT:TopologicalSpace Yh:T = TrivialTopology Yf:X → Y⊢ Continuous f X:TypeY:Typeinst✝:TopologicalSpace XT:TopologicalSpace Yh:T = TrivialTopology Yf:X → Y⊢ ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s) intro U X:TypeY:Typeinst✝:TopologicalSpace XT:TopologicalSpace Yh:T = TrivialTopology Yf:X → YU:Set YhU:IsOpen U⊢ IsOpen (f ⁻¹' U) X:TypeY:Typeinst✝:TopologicalSpace XT:TopologicalSpace Yh:T = TrivialTopology Yf:X → YU:Set YhU:IsOpen U⊢ IsOpen (f ⁻¹' U) X:TypeY:Typeinst✝:TopologicalSpace XT:TopologicalSpace Yh:T = TrivialTopology Yf:X → YU:Set YhUuniv:U = Set.univ⊢ IsOpen (f ⁻¹' U)X:TypeY:Typeinst✝:TopologicalSpace XT:TopologicalSpace Yh:T = TrivialTopology Yf:X → YU:Set YhUempty:U = ∅⊢ IsOpen (f ⁻¹' U) X:TypeY:Typeinst✝:TopologicalSpace XT:TopologicalSpace Yh:T = TrivialTopology Yf:X → YU:Set YhUuniv:U = Set.univ⊢ IsOpen (f ⁻¹' U) -- si U = Y X:TypeY:Typeinst✝:TopologicalSpace XT:TopologicalSpace Yh:T = TrivialTopology Yf:X → YU:Set YhUuniv:U = Set.univ⊢ IsOpen (f ⁻¹' Set.univ) All goals completed! 🐙 X:TypeY:Typeinst✝:TopologicalSpace XT:TopologicalSpace Yh:T = TrivialTopology Yf:X → YU:Set YhUempty:U = ∅⊢ IsOpen (f ⁻¹' U) -- si U = ∅ X:TypeY:Typeinst✝:TopologicalSpace XT:TopologicalSpace Yh:T = TrivialTopology Yf:X → YU:Set YhUempty:U = ∅⊢ IsOpen (f ⁻¹' ∅) All goals completed! 🐙

Proposition 3.10🔗

The composition of continuous functions between topological spaces is also a continuous function.

In Mathlib, this result goes by the name Continuous.comp.

Proof. Let f : X \to Y and g : Y \to Z be two continuous functions and consider their composition g \circ f : X \to Z.

Let W be an open set of Z. Since g is continuous, V = g^{-1}(W) is open in Y. Since f is continuous, f^{-1}(V) is open in X. But f^{-1}(V) = f^{-1}(g^{-1}(W)) = (g \circ f)^{-1}(W)

example (X Y Z : Type) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : X → Y) (g : Y → Z) (hf : Continuous f) (hg : Continuous g) : Continuous (g ∘ f) := X:TypeY:TypeZ:Typeinst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace Yinst✝:TopologicalSpace Zf:X → Yg:Y → Zhf:Continuous fhg:Continuous g⊢ Continuous (g ∘ f) X:TypeY:TypeZ:Typeinst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace Yinst✝:TopologicalSpace Zf:X → Yg:Y → Zhf:∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)hg:∀ (s : Set Z), IsOpen s → IsOpen (g ⁻¹' s)⊢ ∀ (s : Set Z), IsOpen s → IsOpen (g ∘ f ⁻¹' s) intro W X:TypeY:TypeZ:Typeinst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace Yinst✝:TopologicalSpace Zf:X → Yg:Y → Zhf:∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)hg:∀ (s : Set Z), IsOpen s → IsOpen (g ⁻¹' s)W:Set ZhW:IsOpen W⊢ IsOpen (g ∘ f ⁻¹' W) X:TypeY:TypeZ:Typeinst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace Yinst✝:TopologicalSpace Zf:X → Yg:Y → Zhf:∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)W:Set ZhW:IsOpen Whg:IsOpen (g ⁻¹' W)⊢ IsOpen (g ∘ f ⁻¹' W) X:TypeY:TypeZ:Typeinst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace Yinst✝:TopologicalSpace Zf:X → Yg:Y → ZW:Set ZhW:IsOpen Whg:IsOpen (g ⁻¹' W)hf:IsOpen (f ⁻¹' g ⁻¹' W)⊢ IsOpen (g ∘ f ⁻¹' W) All goals completed! 🐙

∎

Proposition 3.11 (Characterisation of continuity via closed sets)🔗

Let X and Y be two topological spaces and f : X \to Y a function between them. Then f is continuous if and only if for each closed C \subseteq Y, we have that f^{-1}(C) is closed in X.

In Mathlib, this result goes by the name continuous_iff_isClosed.

Proof. Suppose that f is continuous. Let C be closed in Y. Then C^c is open in Y. Since f is continuous, f^-1(C^c) is open in X. But f^-1(C^c) = f^-1(C)^c, hence f^-1(C) is closed in X. The converse is analogous.

example (X Y : Type) [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Continuous f ↔ ∀ C : Set Y, IsClosed C → IsClosed (f ⁻¹' C) := X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Y⊢ Continuous f ↔ ∀ (C : Set Y), IsClosed C → IsClosed (f ⁻¹' C) X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Y⊢ Continuous f → ∀ (C : Set Y), IsClosed C → IsClosed (f ⁻¹' C)X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Y⊢ (∀ (C : Set Y), IsClosed C → IsClosed (f ⁻¹' C)) → Continuous f; all_goals X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (C : Set Y), IsClosed C → IsClosed (f ⁻¹' C)⊢ Continuous f X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:Continuous f⊢ ∀ (C : Set Y), IsClosed C → IsClosed (f ⁻¹' C) X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)⊢ ∀ (C : Set Y), IsClosed C → IsClosed (f ⁻¹' C) intro C X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)C:Set YhC:IsClosed C⊢ IsClosed (f ⁻¹' C) X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)C:Set YhC:IsOpen Cᶜ⊢ IsOpen (f ⁻¹' C)ᶜ All goals completed! 🐙 X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (C : Set Y), IsClosed C → IsClosed (f ⁻¹' C)⊢ Continuous f X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (C : Set Y), IsClosed C → IsClosed (f ⁻¹' C)⊢ ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s) intro U X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (C : Set Y), IsClosed C → IsClosed (f ⁻¹' C)U:Set YhU:IsOpen U⊢ IsOpen (f ⁻¹' U) X:TypeY:Typeinst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yf:X → Yh:∀ (C : Set Y), IsClosed C → IsClosed (f ⁻¹' C)U:Set YhU:IsClosed Uᶜ⊢ IsClosed (f ⁻¹' U)ᶜ All goals completed! 🐙

∎

Proposition 3.12 (Continuity in subspaces)🔗

Let X and Y be topological spaces and Z a topological subspace of Y. A function f : X \to Z is continuous if and only if it is continuous as a function f : X \to Y.

That is, to prove the continuity condition for f : X \to Z, it suffices to take arbitrary open sets of Y.

Proof. Let us see each implication separately.

lemma continuousInSubspace_iff_trueForSpace {X Y : Type} {Z : Set Y} [TX : TopologicalSpace X] [TY : TopologicalSpace Y] [TZ : TopologicalSpace Z] (hZ : TZ = TopoSubspace TY Z) (f : X → Z) : Continuous f ↔ ∀ U : Set Y, TY.IsOpen U → TX.IsOpen (f ⁻¹' (Subtype.val ⁻¹' U)) := X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Z⊢ Continuous f ↔ ∀ (U : Set Y), TopologicalSpace.IsOpen U → TopologicalSpace.IsOpen (f ⁻¹' Subtype.val ⁻¹' U) X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Z⊢ (∀ (s : Set ↑Z), IsOpen s → IsOpen (f ⁻¹' s)) ↔ ∀ (U : Set Y), TopologicalSpace.IsOpen U → TopologicalSpace.IsOpen (f ⁻¹' Subtype.val ⁻¹' U) X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Z⊢ (∀ (s : Set ↑Z), IsOpen s → IsOpen (f ⁻¹' s)) → ∀ (U : Set Y), TopologicalSpace.IsOpen U → TopologicalSpace.IsOpen (f ⁻¹' Subtype.val ⁻¹' U)X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Z⊢ (∀ (U : Set Y), TopologicalSpace.IsOpen U → TopologicalSpace.IsOpen (f ⁻¹' Subtype.val ⁻¹' U)) → ∀ (s : Set ↑Z), IsOpen s → IsOpen (f ⁻¹' s) all_goals intro h X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Zh:∀ (U : Set Y), TopologicalSpace.IsOpen U → TopologicalSpace.IsOpen (f ⁻¹' Subtype.val ⁻¹' U)U:Set ↑Z⊢ IsOpen U → IsOpen (f ⁻¹' U) X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Zh:∀ (U : Set Y), TopologicalSpace.IsOpen U → TopologicalSpace.IsOpen (f ⁻¹' Subtype.val ⁻¹' U)U:Set ↑ZhU:IsOpen U⊢ IsOpen (f ⁻¹' U)

(\implies) Suppose that f : X \to Z is continuous. Let U be an open set of Y; we want to see that f^-1(U) is open in X. Since f is continuous, it suffices to see that f(f^{-1})(U) is open. But f(f^{-1})(U) = U \cap Y, which is open by the definition of the subspace topology, since U is open.

X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Zh:∀ (s : Set ↑Z), IsOpen s → IsOpen (f ⁻¹' s)U:Set YhU:TopologicalSpace.IsOpen U⊢ TopologicalSpace.IsOpen (f ⁻¹' Subtype.val ⁻¹' U) -- → X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Zh:∀ (s : Set ↑Z), IsOpen s → IsOpen (f ⁻¹' s)U:Set YhU:TopologicalSpace.IsOpen U⊢ IsOpen (Subtype.val ⁻¹' U) X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Zh:∀ (s : Set ↑Z), IsOpen s → IsOpen (f ⁻¹' s)U:Set YhU:TopologicalSpace.IsOpen U⊢ IsOpen (Subtype.val ⁻¹' U) X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Zh:∀ (s : Set ↑Z), IsOpen s → IsOpen (f ⁻¹' s)U:Set YhU:TopologicalSpace.IsOpen U⊢ TopologicalSpace.IsOpen U ∧ Subtype.val '' Subtype.val ⁻¹' U = U ∩ Z X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Zh:∀ (s : Set ↑Z), IsOpen s → IsOpen (f ⁻¹' s)U:Set YhU:TopologicalSpace.IsOpen U⊢ TopologicalSpace.IsOpen UX:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Zh:∀ (s : Set ↑Z), IsOpen s → IsOpen (f ⁻¹' s)U:Set YhU:TopologicalSpace.IsOpen U⊢ Subtype.val '' Subtype.val ⁻¹' U = U ∩ Z X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Zh:∀ (s : Set ↑Z), IsOpen s → IsOpen (f ⁻¹' s)U:Set YhU:TopologicalSpace.IsOpen U⊢ TopologicalSpace.IsOpen U All goals completed! 🐙 X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Zh:∀ (s : Set ↑Z), IsOpen s → IsOpen (f ⁻¹' s)U:Set YhU:TopologicalSpace.IsOpen U⊢ Subtype.val '' Subtype.val ⁻¹' U = U ∩ Z X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Zh:∀ (s : Set ↑Z), IsOpen s → IsOpen (f ⁻¹' s)U:Set YhU:TopologicalSpace.IsOpen U⊢ Z ∩ U = U ∩ Z All goals completed! 🐙

(\impliedby) Suppose now that f : X \to Y is continuous. Let U be an open set in Z. Then, by the definition of the subspace topology, there exists a V open in Y such that U = V \cap Z. Since f is continuous, f^{-1}(V) is open. Then f^{-1}(U) = f^{-1}(V \cap Z) = f^{-1}(V), since f : X \to Z. Hence it is open.

X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Zh:∀ (U : Set Y), TopologicalSpace.IsOpen U → TopologicalSpace.IsOpen (f ⁻¹' Subtype.val ⁻¹' U)U:Set ↑ZhU:IsOpen U⊢ IsOpen (f ⁻¹' U) -- ← X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Zh:∀ (U : Set Y), TopologicalSpace.IsOpen U → TopologicalSpace.IsOpen (f ⁻¹' Subtype.val ⁻¹' U)U:Set ↑ZhU:IsOpen U⊢ IsOpen (f ⁻¹' U) X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Zh:∀ (U : Set Y), TopologicalSpace.IsOpen U → TopologicalSpace.IsOpen (f ⁻¹' Subtype.val ⁻¹' U)U:Set ↑ZV:Set YhV:TopologicalSpace.IsOpen V ∧ Subtype.val '' U = V ∩ Z⊢ IsOpen (f ⁻¹' U) X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Zh:∀ (U : Set Y), TopologicalSpace.IsOpen U → TopologicalSpace.IsOpen (f ⁻¹' Subtype.val ⁻¹' U)U:Set ↑ZV:Set YhV:TopologicalSpace.IsOpen V ∧ Subtype.val '' U = V ∩ Z⊢ IsOpen (f ⁻¹' Subtype.val ⁻¹' (V ∩ Z)) X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Zh:∀ (U : Set Y), TopologicalSpace.IsOpen U → TopologicalSpace.IsOpen (f ⁻¹' Subtype.val ⁻¹' U)U:Set ↑ZV:Set YhV:TopologicalSpace.IsOpen V ∧ Subtype.val '' U = V ∩ Z⊢ IsOpen (f ⁻¹' Subtype.val ⁻¹' V) X:TypeY:TypeZ:Set YTX:TopologicalSpace XTY:TopologicalSpace YTZ:TopologicalSpace ↑ZhZ:TZ = TopoSubspace TY Zf:X → ↑Zh:∀ (U : Set Y), TopologicalSpace.IsOpen U → TopologicalSpace.IsOpen (f ⁻¹' Subtype.val ⁻¹' U)U:Set ↑ZV:Set YhV:TopologicalSpace.IsOpen V ∧ Subtype.val '' U = V ∩ Z⊢ TopologicalSpace.IsOpen V All goals completed! 🐙

∎

Proposition 3.13🔗

Let f : X \to Y be a function between topological spaces and let \mathcal{B} be a base of Y. Then f is continuous if and only if for each basic open set U \in \mathcal{B}, we have that f^{-1}(U) is open in X.

That is, for the definition of continuity of a function it suffices to take the basic open sets.

lemma continuous_iff_trueForBasics {X Y : Type} [T : TopologicalSpace X] [T' : TopologicalSpace Y] (f : X → Y) (B : Set (Set Y)) (hB : isTopoBase B) : Continuous f ↔ ∀ U ∈ B, IsOpen (f ⁻¹' U)

Proof. The first implication is trivial; if the continuity property holds for every open set, it trivially holds for the basic open sets.

X:TypeY:TypeT:TopologicalSpace XT':TopologicalSpace Yf:X → YB:Set (Set Y)hB:isTopoBase B⊢ (∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)) ↔ ∀ U ∈ B, IsOpen (f ⁻¹' U) X:TypeY:TypeT:TopologicalSpace XT':TopologicalSpace Yf:X → YB:Set (Set Y)hB:isTopoBase B⊢ (∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)) → ∀ U ∈ B, IsOpen (f ⁻¹' U)X:TypeY:TypeT:TopologicalSpace XT':TopologicalSpace Yf:X → YB:Set (Set Y)hB:isTopoBase B⊢ (∀ U ∈ B, IsOpen (f ⁻¹' U)) → ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s); all_goals X:TypeY:TypeT:TopologicalSpace XT':TopologicalSpace Yf:X → YB:Set (Set Y)hB:isTopoBase Bh:∀ U ∈ B, IsOpen (f ⁻¹' U)⊢ ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s) X:TypeY:TypeT:TopologicalSpace XT':TopologicalSpace Yf:X → YB:Set (Set Y)hB:isTopoBase Bh:∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)⊢ ∀ U ∈ B, IsOpen (f ⁻¹' U) All goals completed! 🐙

(\impliedby) Let V be open in Y; we want to see that f^{-1}(V) is open in X. Since \mathcal{B} is a base of Y, there exists a family \{B_i\}_i \subseteq \mathcal{B} such that U = \bigcup_i B_i. Then f^{-1}(U) = f^{-1}\big(\bigcup_i B_i\big) = \bigcup_i f^{-1}(B_i), which will be open when each of the components of the union is open. But B_i is open because it belongs to a base, and f is continuous, hence f^{-1}(B_i) is open for each i.

X:TypeY:TypeT:TopologicalSpace XT':TopologicalSpace Yf:X → YB:Set (Set Y)hB:isTopoBase Bh:∀ U ∈ B, IsOpen (f ⁻¹' U)⊢ ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s) intro V X:TypeY:TypeT:TopologicalSpace XT':TopologicalSpace Yf:X → YB:Set (Set Y)hB:isTopoBase Bh:∀ U ∈ B, IsOpen (f ⁻¹' U)V:Set YhV:IsOpen V⊢ IsOpen (f ⁻¹' V) X:TypeY:TypeT:TopologicalSpace XT':TopologicalSpace Yf:X → YB:Set (Set Y)hB:isTopoBase Bh:∀ U ∈ B, IsOpen (f ⁻¹' U)V:Set YhV:IsOpen VUB:Set (Set Y)hUB:UB ⊆ B ∧ V = ⋃₀ UB⊢ IsOpen (f ⁻¹' V) X:TypeY:TypeT:TopologicalSpace XT':TopologicalSpace Yf:X → YB:Set (Set Y)hB:isTopoBase Bh:∀ U ∈ B, IsOpen (f ⁻¹' U)V:Set YhV:IsOpen VUB:Set (Set Y)hUB:UB ⊆ B ∧ V = ⋃₀ UB⊢ IsOpen (⋃ t ∈ UB, f ⁻¹' t) X:TypeY:TypeT:TopologicalSpace XT':TopologicalSpace Yf:X → YB:Set (Set Y)hB:isTopoBase Bh:∀ U ∈ B, IsOpen (f ⁻¹' U)V:Set YhV:IsOpen VUB:Set (Set Y)hUB:UB ⊆ B ∧ V = ⋃₀ UB⊢ ∀ i ∈ UB, IsOpen (f ⁻¹' i) intro A X:TypeY:TypeT:TopologicalSpace XT':TopologicalSpace Yf:X → YB:Set (Set Y)hB:isTopoBase Bh:∀ U ∈ B, IsOpen (f ⁻¹' U)V:Set YhV:IsOpen VUB:Set (Set Y)hUB:UB ⊆ B ∧ V = ⋃₀ UBA:Set YhA:A ∈ UB⊢ IsOpen (f ⁻¹' A) X:TypeY:TypeT:TopologicalSpace XT':TopologicalSpace Yf:X → YB:Set (Set Y)hB:isTopoBase Bh:∀ U ∈ B, IsOpen (f ⁻¹' U)V:Set YhV:IsOpen VUB:Set (Set Y)hUB:UB ⊆ B ∧ V = ⋃₀ UBA:Set YhA:A ∈ UB⊢ A ∈ B All goals completed! 🐙

∎

These last two results can be combined, so that to prove that f : X \to Z \subseteq Y is continuous, it suffices to prove the condition for the basic open sets of Y. This result, which I have proved in Lean and called continuousInSubspace_iff_trueForBase, is one of the ones we will use to prove continuity in Urysohn's lemma.