funUnique_symm_apply

Mathlib.Algebra.Algebra.Pi

URI: https://scilib.ai/kg/mathlib#AlgEquiv.funUnique_symm_apply

English

The symmetry lemma holds: funUnique R ι S is symmetric with Equiv.funUnique.

Русский

Лемма симметрии: funUnique R ι S симметрична Equiv.funUnique.

LaTeX

$$$$ (\mathrm{funUnique}(R, ι, S))^{-1} x = (\mathrm{Equiv}.\mathrm{funUnique}(ι, S))^{-1} x. $$$$

Lean4

@[simp low]
theorem funUnique_symm_apply [Unique ι] (x : S) : (funUnique R ι S).symm x = (Equiv.funUnique ι S).symm x :=
  rfl

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

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

Разделы

Аффилиация

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