not_inseparable

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#IsClosed.not_inseparable

English

If s is closed, and x ∈ s while y ∉ s, then x and y are not inseparable.

Русский

Если s замкнуто и x ∈ s, а y ∉ s, то x и y неразделимы.

LaTeX

$$$\\text{If } \\text{IsClosed}(s),\\ x\\in s,\\ y\\notin s \\Rightarrow \\neg(x \\sim_i y).$$$

Lean4

theorem not_inseparable (hs : IsClosed s) (hx : x ∈ s) (hy : y ∉ s) : ¬(x ~ᵢ y) := fun h =>
  hy <| (h.mem_closed_iff hs).1 hx

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

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

Разделы

Аффилиация

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