surjective_symm_of_source_eq_univ

Mathlib.Logic.Equiv.PartialEquiv

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

English

If the source is universal, then the symmetric map is surjective.

Русский

Если область определения универсальна, тогда симметричная карта сюръективна.

LaTeX

$$$e.\\text{source}=\\mathrm{univ} \\Rightarrow \\text{Surjective}(e^{\\mathrm{symm}}).$$$

Lean4

theorem surjective_symm_of_source_eq_univ (h : e.source = univ) : Surjective e.symm :=
  e.symm.surjective_of_target_eq_univ h

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

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

Разделы

Аффилиация

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