prodComm_symm

Mathlib.Topology.UniformSpace.Equiv

URI: https://scilib.ai/kg/mathlib#UniformEquiv.prodComm_symm

English

The symmetry of the product commutes with taking inverses.

Русский

Симметрия произведения коммутирует со взятием обратной карты.

LaTeX

$$$\\forall {\\alpha \\beta} [UniformSpace \\alpha] [UniformSpace \\beta],\\; (prodComm \\alpha \\beta).\\text{symm} = prodComm \\beta \\alpha$$$

Lean4

@[simp]
theorem prodComm_symm : (prodComm α β).symm = prodComm β α :=
  rfl

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

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

Разделы

Аффилиация

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