le_of_surjective — Mathlib

English

If there is a surjective map from Fin(m) to Fin(n), then n ≤ m.

Русский

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

LaTeX

$$$\forall f:\mathrm{Fin}(m)\to \mathrm{Fin}(n),\;\text{Surjective}(f)\Rightarrow n\le m.$$$

Lean4

/-- If we have a surjective map from `Fin m` to `Fin n`, then `m ≥ n`.
See also `Fintype.card_le_of_surjective` for the generalisation to arbitrary finite types.
-/
theorem le_of_surjective (f : Fin m → Fin n) (hf : Function.Surjective f) : n ≤ m := by
  simpa using Fintype.card_le_of_surjective f hf

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