antisymm

Mathlib.Topology.Inseparable

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

English

If x specializes to y and y specializes to x, then x and y are inseparable.

Русский

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

LaTeX

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

Lean4

theorem antisymm (h₁ : x ⤳ y) (h₂ : y ⤳ x) : x ~ᵢ y :=
  le_antisymm h₁ h₂

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

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

Разделы

Аффилиация

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