unop_surjective

Mathlib.Data.Opposite

URI: https://scilib.ai/kg/mathlib#Opposite.unop_surjective

English

The function that maps from αᵒᵖ to α by unop is surjective.

Русский

Функция unop: αᵒᵖ → α является сюръективной.

LaTeX

$$$\forall x:\; \exists y:\; unop\ y = x$$$

Lean4

theorem unop_surjective : Function.Surjective (unop : αᵒᵖ → α) :=
  equivToOpposite.symm.surjective

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

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

Разделы

Аффилиация

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