iff_isOpen_fiber_apply

Mathlib.Topology.LocallyConstant.Basic

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

English

For any f : X → Y, IsLocallyConstant f is equivalent to ∀ y, IsOpen (f^{-1}({y})).

Русский

Для любого f : X → Y равенство IsLocallyConstant f эквивалентно ∀ y, IsOpen (f^{-1}({y})).

LaTeX

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

Lean4

theorem iff_isOpen_fiber_apply {f : X → Y} : IsLocallyConstant f ↔ ∀ x, IsOpen (f ⁻¹' {f x}) :=
  (IsLocallyConstant.tfae f).out 0 2

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

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

Разделы

Аффилиация

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