restr_coe_symm

Mathlib.Logic.Equiv.PartialEquiv

URI: https://scilib.ai/kg/mathlib#PartialEquiv.restr_coe_symm

English

The restriction’s inverse coincides with the original inverse.

Русский

Обратное ограничение совпадает с исходным обратным отображением.

LaTeX

$$Theorem: restr_coe_symm$$

Lean4

@[simp, mfld_simps]
theorem restr_coe_symm (s : Set α) : ((e.restr s).symm : β → α) = e.symm :=
  rfl

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

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

Разделы

Аффилиация

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