isClosed_setOf_inseparable

Mathlib.Topology.Separation.Basic

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

← MathLib Explorer

English

The set of all pairs (x,y) with Inseparable x y is closed in X×X.

Русский

Множество всех пар (x,y) с неразделимыми x и y замкнуто в X×X.

LaTeX

$$$ IsClosed \\{p : X \\times X \\mid Inseparable(p.1, p.2)\\}. $$$

Lean4

theorem isClosed_setOf_inseparable : IsClosed {p : X × X | Inseparable p.1 p.2} := by
  simp only [← specializes_iff_inseparable, isClosed_setOf_specializes]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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