specializes'

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#Inseparable.specializes'

English

If x is inseparable from y, then y specializes to x.

Русский

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

LaTeX

$$$x \\sim_i y \\Rightarrow y \\triangleright x.$$$

Lean4

theorem specializes' (h : x ~ᵢ y) : y ⤳ x :=
  h.ge

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

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

Разделы

Аффилиация

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