inl_injective

Mathlib.Data.Sum.Basic

URI: https://scilib.ai/kg/mathlib#Sum.inl_injective

English

The left injection inl : α → α ⊕ β is injective.

Русский

Левая инъекция вl: α → α ⊕ β инъективна.

LaTeX

$$$\forall a_1,a_2,\inl(a_1) = \inl(a_2) \Rightarrow a_1 = a_2$$$

Lean4

theorem inl_injective : Function.Injective (inl : α → α ⊕ β) := fun _ _ ↦ inl.inj

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

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

Разделы

Аффилиация

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