nhds_eq

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#Inseparable.nhds_eq

English

If x ~ᵢ y, then nhds x = nhds y.

Русский

Если x ~ᵢ y, то 𝓝 x = 𝓝 y.

LaTeX

$$$\\text{If } x \\sim_i y, \\quad 𝓝 x = 𝓝 y.$$$

Lean4

theorem nhds_eq (h : x ~ᵢ y) : 𝓝 x = 𝓝 y :=
  h

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

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

Разделы

Аффилиация

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