continuous_of_discreteTopology — Mathlib

English

Let α be a space endowed with the discrete topology. Then every function f: α → β into any topological space β is continuous.

Русский

Пусть α имеет дискретную топологию. Тогда любая функция f: α → β непрерывна.

LaTeX

$$$\text{DiscreteTopology}(\alpha) \Rightarrow \forall \beta\,[\text{TopologicalSpace}(\beta)]\,\forall f: \alpha \to \beta,\ \text{Continuous}(f)$$$

Lean4

@[nontriviality, continuity, fun_prop]
theorem continuous_of_discreteTopology [TopologicalSpace β] {f : α → β} : Continuous f :=
  continuous_def.2 fun _ _ => isOpen_discrete _

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