mem_open_iff

Mathlib.Topology.Inseparable

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

English

If x ~ᵢ y and s is open, 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 open, then } x\\in s \\iff y\\in s.$$$

Lean4

theorem mem_open_iff (h : x ~ᵢ y) (hs : IsOpen s) : x ∈ s ↔ y ∈ s :=
  inseparable_iff_forall_isOpen.1 h s hs

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

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

Разделы

Аффилиация

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