withTopCongr_symm

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#Equiv.withTopCongr_symm

English

The lifting is compatible with taking inverses: withTopCongr(e.symm) equals (withTopCongr(e)).symm.

Русский

Переносимость через инверсии сохраняется: withTopCongr(e.symm) равно (withTopCongr(e)).symm.

LaTeX

$$$\text{withTopCongr}(e^{\mathrm{symm}}) = (\text{withTopCongr}(e))^{\mathrm{symm}}$$$

Lean4

@[simp, grind =]
theorem withTopCongr_symm (e : α ≃ β) : withTopCongr e.symm = (withTopCongr e).symm :=
  rfl

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

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

Разделы

Аффилиация

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