iff_isOpen_fiber

Mathlib.Topology.LocallyConstant.Basic

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

English

IsLocallyConstant f iff ∀ y IsOpen (f^{-1}({y})).

Русский

IsLocallyConstant f тогда и только тогда, когда для всех y множество f^{-1}({y}) открыто.

LaTeX

$$$\\IsLocallyConstant(f) \\iff \\forall y, \\IsOpen\\big(f^{-1}(\\{y\\})\\big)$$$

Lean4

theorem iff_isOpen_fiber {f : X → Y} : IsLocallyConstant f ↔ ∀ y, IsOpen (f ⁻¹' { y }) :=
  (IsLocallyConstant.tfae f).out 0 3

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

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

Разделы

Аффилиация

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