specializes

Mathlib.Topology.Inseparable

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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