ofSurjective — Mathlib

English

Let α be finite and f: α → β be surjective. Then β is finite.

Русский

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

LaTeX

$$$\text{Finite}(\alpha) \land \text{Surjective}(f) \Rightarrow \text{Finite}(\beta)$$$

Lean4

/-- If `f : α → β` is a surjection and `α` is a fintype, then `β` is also a fintype. -/
def ofSurjective [DecidableEq β] [Fintype α] (f : α → β) (H : Function.Surjective f) : Fintype β :=
  ⟨univ.image f, fun b =>
    let ⟨_, e⟩ := H b
    e ▸ mem_image_of_mem _ (mem_univ _)⟩

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