mem_open

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#Specializes.mem_open

English

If h: x ⤳ y and s is open with y ∈ s then x ∈ s.

Русский

Если h: x ⤳ y и s открытое с y ∈ s, тогда x ∈ s.

LaTeX

$$$ h:\ x \!⤳\! y \Rightarrow s\text{ открыто}, y\in s \Rightarrow x\in s$$$

Lean4

theorem mem_open (h : x ⤳ y) (hs : IsOpen s) (hy : y ∈ s) : x ∈ s :=
  specializes_iff_forall_open.1 h s hs hy

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

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

Разделы

Аффилиация

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