homOfContinuous — Mathlib

English

Any morphism of compacta (as a morphism in the category) is continuous.

Русский

Любой морфизм компактумов непрерывен.

LaTeX

$$$\\text{continuous_of_hom}(f) : \\text{Continuous } f$$$

Lean4

/-- Any continuous map between Compacta is a morphism of compacta. -/
def homOfContinuous {X Y : Compactum} (f : X → Y) (cont : Continuous f) : X ⟶ Y :=
  { f
    h := by
      rw [continuous_iff_ultrafilter] at cont
      ext (F : Ultrafilter X)
      specialize cont (X.str F) F (le_nhds_of_str_eq F (X.str F) rfl)
      simp only [types_comp_apply]
      exact str_eq_of_le_nhds (Ultrafilter.map f F) _ cont }

Похожие утверждения