not_disjoint

Mathlib.Topology.Inseparable

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

English

If x specializes to y and s is open with y ∈ s, then x ∈ s.

Русский

Если x специализируется на y и s открыто, а y ∈ s, то x ∈ s.

LaTeX

$$$\text{Specializes}(x,y) \to (s\text{ открыто} \land y\in s) \Rightarrow x\in s$$$

Lean4

theorem not_disjoint (h : x ⤳ y) : ¬Disjoint (𝓝 x) (𝓝 y) := fun hd ↦ absurd (hd.mono_right h) <| by simp [NeBot.ne']

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

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

Разделы

Аффилиация

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