vsub_left_injective

Mathlib.Algebra.AddTorsor.Basic

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

← MathLib Explorer

English

Subtracting p is injective: the function x ↦ x −ᵥ p is injective.

Русский

Вычитание точки p слева инъективно: функция x ↦ x −ᵥ p инъективна.

LaTeX

$$$ \text{Injective}((\cdot) -ᵥ p) $$$

Lean4

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

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

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

Разделы

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

Аффилиация

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