mem_closed_iff

Mathlib.Topology.Inseparable

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

English

If x ~ᵢ y and s is closed, then x ∈ s iff y ∈ s.

Русский

Если x ~ᵢ y и s замкнуто, то x ∈ s тогда и только тогда, когда y ∈ s.

LaTeX

$$$\\text{If } x \\sim_i y \\text{ and } s \\text{ is closed, then } x\\in s \\iff y\\in s.$$$

Lean4

theorem mem_closed_iff (h : x ~ᵢ y) (hs : IsClosed s) : x ∈ s ↔ y ∈ s :=
  inseparable_iff_forall_isClosed.1 h s hs

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

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

Разделы

Аффилиация

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