mem_nhdsKer_singleton

Mathlib.Topology.NhdsKer

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

English

x ∈ nhdsKer({y}) iff x specializes to y.

Русский

x принадлежит nhdsKer({y}) тогда и только тогда, когда x специализируется на y.

LaTeX

$$x ∈ nhdsKer(\\{y\\}) \\iff x ⤳ y$$

Lean4

@[simp]
theorem mem_nhdsKer_singleton : x ∈ nhdsKer { y } ↔ x ⤳ y := by
  rw [nhdsKer_singleton_eq_ker_nhds, ker_nhds_eq_specializes, mem_setOf]

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

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

Разделы

Аффилиация

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