cast_symm

Mathlib.Logic.Equiv.Defs

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

English

The inverse of a cast is the cast of the inverse: cast(h).symm = cast(h.symm).

Русский

Обратное от приведения равно приведению обратного: cast(h).symm = cast(h.symm).

LaTeX

$$$\\operatorname{cast}(h)^{-1} = \\operatorname{cast}(h^{-1}).$$$

Lean4

@[simp]
theorem cast_symm {α β} (h : α = β) : (Equiv.cast h).symm = Equiv.cast h.symm :=
  rfl

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

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

Разделы

Аффилиация

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