le_of_embedding — Mathlib

English

If there is an embedding from Fin(m) to Fin(n), then m ≤ n.

Русский

Если существует вложение (встраивание) Fin(m) в Fin(n), то m ≤ n.

LaTeX

$$$\forall m,n\in\mathbb N\; (f:\mathrm{Fin}(m)\hookrightarrow \mathrm{Fin}(n))\Rightarrow m \le n.$$$

Lean4

/-- If we have an embedding from `Fin m` to `Fin n`, then `m ≤ n`.
See also `Fintype.card_le_of_embedding` for the generalisation to arbitrary finite types.
-/
theorem le_of_embedding (f : Fin m ↪ Fin n) : m ≤ n := by simpa using Fintype.card_le_of_embedding f

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