continuous_iff — Mathlib

English

If S is coherent, a map f: X→Y is continuous if and only if its restrictions to all s∈S are continuous.

Русский

Если S когерентно, то отображение f: X→Y непрерывно тогда и только тогда, когда его ограничения на все s∈S непрерывны.

LaTeX

$$$ \\text{Continuous}(f) \\iff \\forall s \\in S, \\text{ContinuousOn}(f, s) $$$

Lean4

protected theorem continuous_iff {Y : Type*} [TopologicalSpace Y] {f : X → Y} (hS : IsCoherentWith S) :
    Continuous f ↔ ∀ s ∈ S, ContinuousOn f s :=
  ⟨fun h _ _ ↦ h.continuousOn, fun h ↦
    continuous_def.2 fun _u hu ↦ hS.isOpen_iff.2 fun s hs ↦ hu.preimage <| (h s hs).restrict⟩

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