symm

Mathlib.SetTheory.ZFC.PSet

URI: https://scilib.ai/kg/mathlib#PSet.Equiv.symm

English

Equivalence is symmetric: x ≃ y implies y ≃ x.

Русский

Эквивалентность симметрична: x ≃ y ⇒ y ≃ x.

LaTeX

$$Equiv x y → Equiv y x$$

Lean4

@[symm]
protected theorem symm {x y} : Equiv x y → Equiv y x :=
  (Equiv.refl y).euc

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

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

Разделы

Аффилиация

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