iff_continuous — Mathlib

English

For any X and Y with Y discrete, f is locally constant iff f is continuous.

Русский

Для X и Y с дискретной топологией кодома, f локально константна тогда и только тогда, когда она непрерывна.

LaTeX

$$$\\text{IsLocallyConstant}(f) \\iff \\text{Continuous}(f)$ under the assumption $[DiscreteTopology\\,Y]$.$$

Lean4

theorem iff_continuous {_ : TopologicalSpace Y} [DiscreteTopology Y] (f : X → Y) : IsLocallyConstant f ↔ Continuous f :=
  ⟨IsLocallyConstant.continuous, fun h s => h.isOpen_preimage s (isOpen_discrete _)⟩

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