lt_of_injective_of_notMem — Mathlib

English

If there is an injective map Fin(m) → Fin(n) whose image omits at least one element of Fin(n), then m < n.

Русский

Если существует инъективное отображение Fin(m) → Fin(n), чья образ не содержит всю Fin(n), то m < n.

LaTeX

$$$\forall f:\mathrm{Fin}(m)\to \mathrm{Fin}(n),\;\text{Injective}(f)\Rightarrow\forall b:\mathrm{Fin}(n), b\notin\mathrm{range}(f)\Rightarrow m

Lean4

/-- If we have an injective map from `Fin m` to `Fin n` whose image does not contain everything,
then `m < n`. See also `Fintype.card_lt_of_injective_of_notMem` for the generalisation to
arbitrary finite types.
-/
theorem lt_of_injective_of_notMem (f : Fin m → Fin n) (hf : f.Injective) {b : Fin n} (hb : b ∉ Set.range f) : m < n :=
  by simpa using Fintype.card_lt_of_injective_of_notMem f hf hb

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