English
If X has the discrete topology, any function f : X → Y is locally constant.
Русский
Если X имеет дискретную топологию, любая функция f : X → Y локально константна.
LaTeX
$$$[\\text{DiscreteTopology } X]\\;\\Rightarrow\\; \\operatorname{IsLocallyConstant}(f)$$$
Lean4
protected theorem tfae (f : X → Y) :
TFAE
[IsLocallyConstant f, ∀ x, ∀ᶠ x' in 𝓝 x, f x' = f x, ∀ x, IsOpen {x' | f x' = f x}, ∀ y, IsOpen (f ⁻¹' { y }),
∀ x, ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x] :=
by
tfae_have 1 → 4 := fun h y => h { y }
tfae_have 4 → 3 := fun h x => h (f x)
tfae_have 3 → 2 := fun h x => IsOpen.mem_nhds (h x) rfl
tfae_have 2 → 5
| h, x => by
rcases mem_nhds_iff.1 (h x) with ⟨U, eq, hU, hx⟩
exact ⟨U, hU, hx, eq⟩
tfae_have 5 → 1
| h, s => by
refine isOpen_iff_forall_mem_open.2 fun x hx ↦ ?_
rcases h x with ⟨U, hU, hxU, eq⟩
exact ⟨U, fun x' hx' => mem_preimage.2 <| (eq x' hx').symm ▸ hx, hU, hxU⟩
tfae_finish
