range_finite — Mathlib

English

If X is compact and f: X → Y is locally constant, then the range of f is finite.

Русский

Если X компактно, а f: X → Y локально константна, то множество значений f на X конечно.

LaTeX

$$$[CompactSpace X] {f : X → Y} IsLocallyConstant f → (Set.range f).Finite$$

Lean4

theorem range_finite [CompactSpace X] {f : X → Y} (hf : IsLocallyConstant f) : (Set.range f).Finite :=
  by
  letI : TopologicalSpace Y := ⊥; haveI := discreteTopology_bot Y
  exact (isCompact_range hf.continuous).finite_of_discrete

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