vsub_right_injective

Mathlib.Algebra.AddTorsor.Basic

URI: https://scilib.ai/kg/mathlib#vsub_right_injective

← MathLib Explorer

English

Subtracting p on the right is injective: the function p1 ↦ p −ᵥ p1 is injective.

Русский

Правое вычитание p инъективно: функция p1 ↦ p −ᵥ p1 инъективна.

LaTeX

$$$ \text{Injective}((p -ᵥ \cdot) : P \to G) $$$

Lean4

/-- Subtracting a point from the point `p` is an injective
function. -/
theorem vsub_right_injective (p : P) : Function.Injective ((p -ᵥ ·) : P → G) := fun _ _ => vsub_right_cancel

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

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

Разделы

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

Аффилиация

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