op_surjective

Mathlib.Data.Opposite

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

English

The function that sends an element to its opposite is surjective.

Русский

Функция перевода в противоположное множество на всю область покрытия.

LaTeX

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

Lean4

theorem op_surjective : Function.Surjective (op : α → αᵒᵖ) :=
  equivToOpposite.surjective

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

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

Разделы

Аффилиация

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