symm

Mathlib.Topology.DiscreteQuotient

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

English

If x is related to y, then y is related to x.

Русский

Если x эквивалентен y, то y эквивалентен x.

LaTeX

$$$ x \\sim_S y \\Rightarrow y \\sim_S x $$$

Lean4

theorem symm (x y : X) : S.toSetoid x y → S.toSetoid y x :=
  S.symm'

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

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

Разделы

Аффилиация

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