bijOn

Mathlib.Logic.Equiv.PartialEquiv

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

English

The forward map is a bijection between the source and target.

Русский

Преобразование является биекцией между источником и целью.

LaTeX

$$$\text{BijOn } e\, e. source\ e. target$$$

Lean4

protected theorem bijOn : BijOn e e.source e.target :=
  e.invOn.bijOn e.mapsTo e.symm_mapsTo

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

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

Разделы

Аффилиация

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