specializes_iff_nhds

Mathlib.Topology.Inseparable

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

English

If x specializes to y, then the neighborhood filters at x and y are not disjoint.

Русский

Если x специализируется на y, то фильтры окрестностей в x и y не несовпадают по пересечению.

LaTeX

$$$\text{Specializes}(x,y) \Rightarrow \lnot \text{Disjoint}(\mathcal{N}(x), \mathcal{N}(y))$$$

Lean4

theorem specializes_iff_nhds : x ⤳ y ↔ 𝓝 x ≤ 𝓝 y :=
  Iff.rfl

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

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

Разделы

Аффилиация

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