card_lt_of_surjective_not_injective

English

Let α,β be finite and f: α → β be surjective and not injective. Then |β| < |α|.

Русский

Пусть α,β конечны и f: α → β сюрьективно, но не инъективно. Тогда |β| < |α|.

LaTeX

$$$[Fintype\\alpha][Fintype\\beta]\\ (f:\\alpha \\to \\beta)\\ (hf: Surjective f) (h': \\neg Injective f)\\Rightarrow |\\beta| < |\\alpha|$$$

Lean4

theorem card_lt_of_surjective_not_injective [Fintype α] [Fintype β] (f : α → β) (h : Function.Surjective f)
    (h' : ¬Function.Injective f) : card β < card α :=
  card_lt_of_injective_not_surjective _ (Function.injective_surjInv h) fun hg =>
    have w : Function.Bijective (Function.surjInv h) := ⟨Function.injective_surjInv h, hg⟩
    h' <| h.injective_of_fintype (Equiv.ofBijective _ w).symm

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