refl

Mathlib.Topology.Inseparable

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

English

If x ~ᵢ y, then the neighborhoods of x and y agree: nhds x = nhds y.

Русский

Если x ~ᵢ y, то множества окрестностей x и y совпадают: 𝓝 x = 𝓝 y.

LaTeX

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

Lean4

@[refl]
theorem refl (x : X) : x ~ᵢ x :=
  Eq.refl (𝓝 x)

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

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

Разделы

Аффилиация

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