inr_injective

Mathlib.Data.Sum.Basic

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

English

The right injection inr : β → α ⊕ β is injective.

Русский

Правая инъекция inr: β → α ⊕ β инъективна.

LaTeX

$$$\forall b_1,b_2,\ inr(b_1) = inr(b_2) \Rightarrow b_1 = b_2$$$

Lean4

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

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

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

Разделы

Аффилиация

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