English
There exists an embedding Fin n → Fin m if and only if n ≤ m.
Русский
Существует вложение Fin n → Fin m тогда и только тогда, когда n ≤ m.
LaTeX
$$$ \text{Nonempty}(\mathrm{Fin}(n) \hookrightarrow \mathrm{Fin}(m)) \iff n \le m $$$
Lean4
theorem nonempty_embedding_iff : Nonempty (Fin n ↪ Fin m) ↔ n ≤ m :=
by
refine ⟨fun h ↦ ?_, fun h ↦ ⟨castLEEmb h⟩⟩
induction n generalizing m with
| zero => exact m.zero_le
| succ n ihn =>
obtain ⟨e⟩ := h
rcases exists_eq_succ_of_ne_zero (pos_iff_nonempty.2 (Nonempty.map e inferInstance)).ne' with ⟨m, rfl⟩
refine Nat.succ_le_succ <| ihn ⟨?_⟩
refine ⟨fun i ↦ (e.setValue 0 0 i.succ).pred (mt e.setValue_eq_iff.1 i.succ_ne_zero), fun i j h ↦ ?_⟩
simpa only [pred_inj, EmbeddingLike.apply_eq_iff_eq, succ_inj] using h
