continuous_iff_of_isColimit — Mathlib

English

For a function f: c.pt → X into a topological space X, f is continuous iff for every j in J, the composite f ∘ c.ι.app j is continuous.

Русский

Для функции f: c.pt → X в топологическое пространство X, непрерывна тогда и только тогда, когда композиция f ∘ c.ι.app j непрерывна для каждого j.

LaTeX

$$$ \text{Continuous } f \;\iff\; \forall j, \text{Continuous } (f \circ c.\iota.app j) $$$

Lean4

theorem continuous_iff_of_isColimit {X : Type u'} [TopologicalSpace X] (f : c.pt → X) :
    Continuous f ↔ ∀ (j : J), Continuous (f ∘ c.ι.app j) :=
  by
  simp only [continuous_def, isOpen_iff_of_isColimit _ hc]
  tauto

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