injective_of_lt_imp_ne — Mathlib

English

If a linear order α satisfies x < y → f x ≠ f y, then f is injective.

Русский

Если для линейного порядка α выполняется x < y ⇒ f(x) ≠ f(y), то f инъективна.

LaTeX

$$[LinearOrder α] {f : α → β} (h : ∀ x y, x < y → f x ≠ f y) → Injective f$$

Lean4

theorem injective_of_lt_imp_ne [LinearOrder α] {f : α → β} (h : ∀ x y, x < y → f x ≠ f y) : Injective f :=
  by
  intro x y hf
  rcases lt_trichotomy x y with (hxy | rfl | hxy)
  · exact absurd hf <| h _ _ hxy
  · rfl
  · exact absurd hf.symm <| h _ _ hxy

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