IsLocallyConstant — Mathlib

English

A function f : X → Y is locally constant if and only if for every x ∈ X there exists an open set U containing x such that f is constant on U.

Русский

Функция f : X → Y является локально константной тогда и только тогда, когда для каждого x ∈ X существует открытое множество U, содержащее x, такое что f устойчиво постоянна на U.

LaTeX

$$$\\IsLocallyConstant(f) \\iff \\forall x, \\exists U\\,\\IsOpen(U) \\wedge x \\in U \\\\quad\\land \\forall x' \\in U, f(x') = f(x)$$$

Lean4

/-- A function between topological spaces is locally constant if the preimage of any set is open. -/
def IsLocallyConstant (f : X → Y) : Prop :=
  ∀ s : Set Y, IsOpen (f ⁻¹' s)

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