injective_symm_of_target_eq_univ

Mathlib.Logic.Equiv.PartialEquiv

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

English

If e.target = univ, then e.symm is injective.

Русский

Если e.цель равна универсу, то e.symm инъективен.

LaTeX

$$$e.\\text{target}=\\mathrm{univ} \\Rightarrow \\text{Injective}(e^{\\mathrm{symm}}).$$$

Lean4

theorem injective_symm_of_target_eq_univ (h : e.target = univ) : Injective e.symm :=
  e.symm.injective_of_source_eq_univ h

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

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

Разделы

Аффилиация

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