English
For an order-homomorphism f: Fin(n+1) → α with α a partial order, f is injective iff for all i ∈ Fin n, f(i.castSucc) ≠ f(i.succ).
Русский
Для отображения порядка f: Fin(n+1) → α с частичным порядком α, тождественность f эквивалентна тому, что для всех i в Fin n элементы f(i.castSucc) и f(i.succ) различны.
LaTeX
$$$\mathrm{Injective}(f) \iff \forall i : \mathrm{Fin}\ n, f(i.castSucc) \neq f(i.succ)$$$
Lean4
theorem orderHom_injective_iff {α : Type*} [PartialOrder α] {n : ℕ} (f : Fin (n + 1) →o α) :
Function.Injective f ↔ ∀ (i : Fin n), f i.castSucc ≠ f i.succ :=
by
constructor
· intro hf i hi
have := hf hi
simp [Fin.ext_iff] at this
· intro hf
refine (strictMono_iff_lt_succ (f := f).2 fun i ↦ ?_).injective
exact lt_of_le_of_ne (f.monotone (Fin.castSucc_le_succ i)) (hf i)
