specializes_iff_inseparable

Mathlib.Topology.Separation.Basic

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

← MathLib Explorer

English

In an R0 space, Specializes is equivalent to Inseparable.

Русский

В пространстве R0 Specializes эквивалентна Inseparable.

LaTeX

$$$x \\mathrel{\\rhd} y \\iff Inseparable(x,y)$$$

Lean4

/-- In an R₀ space, `Specializes` is equivalent to `Inseparable`. -/
theorem specializes_iff_inseparable : x ⤳ y ↔ Inseparable x y :=
  ⟨fun h ↦ h.antisymm h.symm, Inseparable.specializes⟩

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

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

Разделы

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

Аффилиация

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