isOpen_fiber

Mathlib.Topology.LocallyConstant.Basic

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

English

If f is locally constant, then for any y ∈ Y the fiber {x | f(x) = y} is open.

Русский

Если f локально константна, тогда множество волокна {x | f(x) = y} открыто для любого y ∈ Y.

LaTeX

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

Lean4

theorem isOpen_fiber {f : X → Y} (hf : IsLocallyConstant f) (y : Y) : IsOpen {x | f x = y} :=
  hf { y }

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

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

Разделы

Аффилиация

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