of_injective — Mathlib

English

If f: α → β is injective and β is finite, then α is finite.

Русский

Если функция f: α → β инъективна и β конечен, то α конечен.

LaTeX

$$$\operatorname{Finite}(\beta) \land \operatorname{Injective}(f) \Rightarrow \operatorname{Finite}(\alpha).$$$

Lean4

theorem of_injective {α β : Sort*} [Finite β] (f : α → β) (H : Injective f) : Finite α :=
  by
  rcases Finite.exists_equiv_fin β with ⟨n, ⟨e⟩⟩
  classical exact .of_equiv (Set.range (e ∘ f)) (Equiv.ofInjective _ (e.injective.comp H)).symm

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