isClopen_fiber — Mathlib

English

For locally constant f, the fiber {x | f(x) = y} is clopen (both open and closed) for every y.

Русский

Для локально константной f волокно {x | f(x) = y} является и открытым, и замкнутым для каждого y.

LaTeX

$$$\\forall y, \\ \\{x : X \\mid f(x) = y\\} \\text{ isClopen}$$$

Lean4

theorem isClopen_fiber {f : X → Y} (hf : IsLocallyConstant f) (y : Y) : IsClopen {x | f x = y} :=
  ⟨isClosed_fiber hf _, isOpen_fiber hf _⟩

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