ofBijective — Mathlib

English

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

Русский

Пусть f: α → β – биекция и α конечно. Тогда β конечно.

LaTeX

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

Lean4

/-- If `f : α → β` is a bijection and `α` is a fintype, then `β` is also a fintype. -/
def ofBijective [Fintype α] (f : α → β) (H : Function.Bijective f) : Fintype β :=
  ⟨univ.map ⟨f, H.1⟩, fun b =>
    let ⟨_, e⟩ := H.2 b
    e ▸ mem_map_of_mem _ (mem_univ _)⟩

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