Continuity of composition

3/4 ~15 minlean

Use the library API to prove composition preserves continuity.

8 lines · Lean 4

import Mathlib

example {α β γ : Type} [TopologicalSpace α]
    [TopologicalSpace β] [TopologicalSpace γ]
    {f : α → β} {g : β → γ}
    (hf : Continuous f) (hg : Continuous g) :
    Continuous (g ∘ f) := by
  sorry

Objectifs

Use the library API to prove composition preserves continuity.

Indices

Voir la solution

import Mathlib

example {α β γ : Type} [TopologicalSpace α]
    [TopologicalSpace β] [TopologicalSpace γ]
    {f : α → β} {g : β → γ}
    (hf : Continuous f) (hg : Continuous g) :
    Continuous (g ∘ f) := by
  exact hg.comp hf