comm'

Mathlib.Data.Setoid.Basic

URI: https://scilib.ai/kg/mathlib#Setoid.comm'

English

s x y ↔ s y x; symmetry of the equivalence relation.

Русский

s x y эквивалентно s y x; симметрия эквивалентности.

LaTeX

$$$ s(x,y) \iff s(y,x) $$$

Lean4

theorem comm' (s : Setoid α) {x y} : s x y ↔ s y x :=
  ⟨s.symm', s.symm'⟩

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

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

Разделы

Аффилиация

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