injective_add_right_of_ne_top

Mathlib.Algebra.Order.AddGroupWithTop

URI: https://scilib.ai/kg/mathlib#LinearOrderedAddCommGroupWithTop.injective_add_right_of_ne_top

← MathLib Explorer

English

If b is not top, the map x ↦ b + x is injective.

Русский

Если b не равен ⊤, отображение x ↦ b + x инъективно.

LaTeX

$$$b \neq \top \implies \mathrm{Injective}(\lambda x. b + x)$$$

Lean4

theorem injective_add_right_of_ne_top (b : α) (h : b ≠ ⊤) : Function.Injective (fun x ↦ b + x) := by
  simpa [add_comm] using injective_add_left_of_ne_top b h

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

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

Разделы

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

Аффилиация

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