le_of_injective — Mathlib

English

If there is an injective map 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)\to \mathrm{Fin}(n))\;\Rightarrow\;\mathrm{Injective}(f)\Rightarrow m \le n.$$$

Lean4

/-- If we have an injective map from `Fin m` to `Fin n`, then `m ≤ n`.
See also `Fintype.card_le_of_injective` for the generalisation to arbitrary finite types.
-/
theorem le_of_injective (f : Fin m → Fin n) (hf : f.Injective) : m ≤ n := by
  simpa using Fintype.card_le_of_injective f hf

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