ι_injective

Mathlib.Topology.Category.CompHausLike.Limits

URI: https://scilib.ai/kg/mathlib#CompHausLike.finiteCoproduct.ι_injective

English

Each inclusion map into a finite coproduct is injective on points.

Русский

Кажторское вложение в конечном копроизведении инъективно по точкам.

LaTeX

$$$\\forall a:\\alpha,\\; Function.Injective(\\mathrm{finiteCoproduct}.\\iota X a)$$$

Lean4

theorem ι_injective (a : α) : Function.Injective (finiteCoproduct.ι X a) :=
  by
  intro x y hxy
  exact eq_of_heq (Sigma.ext_iff.mp hxy).2

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

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

Разделы

Аффилиация

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