symm

Mathlib.Topology.Inseparable

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

English

If x ~ᵢ y then y ~ᵢ x.

Русский

Если x ~ᵢ y, то y ~ᵢ x.

LaTeX

$$$\\text{If } x \\sim_i y, \\text{ then } y \\sim_i x.$$$

Lean4

@[symm]
nonrec theorem symm (h : x ~ᵢ y) : y ~ᵢ x :=
  h.symm

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

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

Разделы

Аффилиация

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