not_specializes

Mathlib.Topology.Inseparable

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

English

If s is closed and x ∈ s but y ∉ s, then x does not specialize to y.

Русский

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

LaTeX

$$$ IsClosed(s) \land x \in s \land y \notin s \Rightarrow \neg x ⤳ y$$$

Lean4

theorem not_specializes (hs : IsClosed s) (hx : x ∈ s) (hy : y ∉ s) : ¬x ⤳ y := fun h => hy <| h.mem_closed hs hx

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

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

Разделы

Аффилиация

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