injective_pair_iff_ne — Mathlib

English

The injectivity of the map i ↦ [x,y] is equivalent to x ≠ y; i.e., function Injective([x,y]) ⇔ x ≠ y.

Русский

Инъективность отображения i ↦ [x,y] эквивалентна x ≠ y; то есть Injective([x,y]) ⇔ x ≠ y.

LaTeX

$$$\mathrm{Injective}([x,y]) \iff x \neq y$$$

Lean4

@[simp]
theorem injective_pair_iff_ne {α : Type*} {x y : α} : Function.Injective ![x, y] ↔ x ≠ y :=
  by
  refine ⟨fun h ↦ ?_, fun h a b h' ↦ ?_⟩
  · simpa using h.ne Fin.zero_ne_one
  · fin_cases a <;> fin_cases b <;> aesop

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