English
Let f: X → B where B carries the discrete topology. Then f is continuous if and only if for every b ∈ B the preimage f^{-1}({b}) is open in X.
Русский
Пусть f: X → B, где B имеет дискретную топологию. Тогда f непрерывна тогда и только тогда, когда прообраз каждого множества-одиночности {b} открыт в X.
LaTeX
$$$\mathrm{Continuous}(f) \iff \forall b \in \beta,\; \IsOpen\bigl(f^{-1} \{b\}\bigr)$$$
Lean4
/-- A function to a discrete topological space is continuous if and only if the preimage of every
singleton is open. -/
theorem continuous_discrete_rng {α} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology β] {f : α → β} :
Continuous f ↔ ∀ b : β, IsOpen (f ⁻¹' { b }) :=
⟨fun h _ => (isOpen_discrete _).preimage h, fun h =>
⟨fun s _ => by
rw [← biUnion_of_singleton s, preimage_iUnion₂]
exact isOpen_biUnion fun _ _ => h _⟩⟩
