injOn

Mathlib.Logic.Equiv.PartialEquiv

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

English

e is injective on its source.

Русский

e инъективна на своем источнике.

LaTeX

$$$\text{InjOn } e\, e. source$$$

Lean4

protected theorem injOn : InjOn e e.source :=
  e.leftInvOn.injOn

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

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

Разделы

Аффилиация

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