ker_nhds_eq_specializes

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#ker_nhds_eq_specializes

English

The kernel of nhds x equals the set of all y such that y specializes to x.

Русский

Ядро nhds x совпадает с множеством y, которые специализируются на x.

LaTeX

$$$ (\mathcal{N}(x)).ker = \{ y \mid y \;⤳\; x \}$$$

Lean4

theorem ker_nhds_eq_specializes : (𝓝 x).ker = {y | y ⤳ x} := by ext; simp [specializes_iff_pure, le_def]

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

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

Разделы

Аффилиация

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