English
If e is an order isomorphism between Fin(n) and Fin(m), then n = m and e acts as the identity on indices; in particular, (e i) as a natural number equals i for every i ∈ Fin(n).
Русский
Если e — ордизоморфизм между Fin(n) и Fin(m), то n = m и e действует как тождественное отображение на индексах; в частности, для каждого i ∈ Fin(n) имеем e(i) = i в виде натурального числа.
LaTeX
$$$\forall e: \mathrm{Fin}(n) \cong_o \mathrm{Fin}(m),\; n = m \land (\forall i \in \mathrm{Fin}(n), e(i)=i).$$$
Lean4
/-- If `e` is an `orderIso` between `Fin n` and `Fin m`, then `n = m` and `e` is the identity
map. In this lemma we state that for each `i : Fin n` we have `(e i : ℕ) = (i : ℕ)`. -/
@[simp]
theorem coe_orderIso_apply (e : Fin n ≃o Fin m) (i : Fin n) : (e i : ℕ) = i :=
by
rcases i with ⟨i, hi⟩
dsimp only
induction i using Nat.strong_induction_on with
| _ i h
refine le_antisymm (forall_lt_iff_le.1 fun j hj => ?_) (forall_lt_iff_le.1 fun j hj => ?_)
· have := e.symm.lt_symm_apply.1 (mk_lt_of_lt_val hj)
specialize h _ this (e.symm _).is_lt
simp only [Fin.eta, OrderIso.apply_symm_apply] at h
rwa [h]
· rwa [← h j hj (hj.trans hi), ← lt_iff_val_lt_val, e.lt_iff_lt]
