unop_injective

Mathlib.Data.Opposite

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

English

The map that sends an opposite element back to its original is injective.

Русский

Отображение xᵒᵖ ↦ x обратно в оригинал является инъекцией.

LaTeX

$$$\text{Function.Injective}(\mathrm{unop} : α^\mathrm{op} \to α)$$$

Lean4

theorem unop_injective : Function.Injective (unop : αᵒᵖ → α) := fun ⟨_⟩ ⟨_⟩ => by simp

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

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

Разделы

Аффилиация

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