graph_inv

Mathlib.Data.Rel

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

English

For an equivalence f, the graph of its inverse equals the inverse of the graph of f.

Русский

Для эквивалентности f граф обратной функции равен обратному графу самой функции.

LaTeX

$$$ (f : \alpha \simeq \beta).\text{symm}.graph = \mathrm{SetRel.inv} (f.graph)$$$

Lean4

theorem graph_inv (f : α ≃ β) : (f.symm : β → α).graph = SetRel.inv (f : α → β).graph := by aesop

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

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

Разделы

Аффилиация

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