inl_injective

Mathlib.Algebra.GroupWithZero.ProdHom

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

← MathLib Explorer

English

The left injection inl: G → G × H is injective.

Русский

Левая инъекция inl: G → G × H инъективна.

LaTeX

$$$\forall g_1,g_2,\ \mathrm{inl}(g_1) = \mathrm{inl}(g_2) \Rightarrow g_1 = g_2$$$

Lean4

theorem inl_injective [DecidablePred fun x : G₀ ↦ x = 0] : Function.Injective (inl G₀ H₀) :=
  Function.HasLeftInverse.injective ⟨fst .., fun _ ↦ by simp⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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