inl_injective

Mathlib.LinearAlgebra.Prod

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

English

The left injection is injective: x ≠ y implies inl x ≠ inl y.

Русский

Левое вложение инъективно: $x≠y$ тогда $inl(x)≠inl(y)$.

LaTeX

$$$\\forall x,y\\in M,\\ inl\\, x = inl\\, y\\Rightarrow x=y$$$

Lean4

theorem inl_injective : Function.Injective (inl R M M₂) := fun _ => by simp

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

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

Разделы

Аффилиация

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