invOn

Mathlib.Logic.Equiv.PartialEquiv

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

English

Combining LeftInvOn and RightInvOn yields the inverse property on the whole source-target pair.

Русский

Сочетание LeftInvOn и RightInvOn дает свойства обратного отображения на паре источник-цель.

LaTeX

$$$\text{InvOn } e.symm\, e\, e. source\ e. target$$$

Lean4

protected theorem invOn : InvOn e.symm e e.source e.target :=
  ⟨e.leftInvOn, e.rightInvOn⟩

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

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

Разделы

Аффилиация

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