add_left_injective_of_ne_top — Mathlib

English

For any n with n ≠ ⊤, the map x ↦ x + n is injective.

Русский

Для любого n, где n ≠ ⊤, отображение x ↦ x + n инъективно.

LaTeX

$$$$\forall n \in \mathbb{N}_\infty,\ n \ne \top \Rightarrow \text{Injective}(\lambda x, x + n).$$$$

Lean4

theorem add_left_injective_of_ne_top {n : ℕ∞} (hn : n ≠ ⊤) : Function.Injective (· + n) :=
  by
  intro a b e
  exact le_antisymm ((WithTop.add_le_add_iff_right hn).mp e.le) ((WithTop.add_le_add_iff_right hn).mp e.ge)

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