continuous — Mathlib

English

A locally constant function is continuous, and conversely, if the codomain is discrete, local constancy is equivalent to continuity.

Русский

Локально константная функция непрерывна; причём если кодом пространства Y дискретно, локальная константность эквивалентна непрерывности.

LaTeX

$$$\\IsLocallyConstant(f) \\Rightarrow \\text{Continuous}(f)$, and if $[DiscreteTopology\,Y]$, $\\IsLocallyConstant(f) \\iff \\text{Continuous}(f)$.$$

Lean4

protected theorem continuous [TopologicalSpace Y] {f : X → Y} (hf : IsLocallyConstant f) : Continuous f :=
  ⟨fun _ _ => hf _⟩

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