subtype_injective

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

URI: https://scilib.ai/kg/mathlib#AffineSubspace.subtype_injective

English

The inclusion map s.subtype: s → P is injective; distinct points of s have distinct images in P.

Русский

Включение s.subtype: s → P инъективно; разные точки в s имеют разные образы в P.

LaTeX

$$$ p,q \\in s \\\\text{and } s.subtype(p) = s.subtype(q) \\Rightarrow p = q $$$

Lean4

theorem subtype_injective (s : AffineSubspace k P) [Nonempty s] : Function.Injective s.subtype :=
  Subtype.coe_injective

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

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

Разделы

Аффилиация

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