isClosed_fiber

Mathlib.Topology.LocallyConstant.Basic

URI: https://scilib.ai/kg/mathlib#IsLocallyConstant.isClosed_fiber

English

If f is locally constant, then the fiber {x | f(x) = y} is closed for every y.

Русский

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

LaTeX

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

Lean4

theorem isClosed_fiber {f : X → Y} (hf : IsLocallyConstant f) (y : Y) : IsClosed {x | f x = y} :=
  ⟨hf { y }ᶜ⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru