univ_map_embedding — Mathlib

English

For a finite α, any embedding e: α ↪ α has image equal to α; i.e., such an embedding is surjective.

Русский

Для конечного множества α любой вложение e: α ↪ α имеет образ равный α; то есть e сюрьективно отображает α на α.

LaTeX

$$$[Fintype\\alpha]\\ (e:\\alpha \\hookrightarrow \\alpha)\\Rightarrow \\operatorname{range}(e)=\\alpha$$$

Lean4

@[simp]
theorem univ_map_embedding {α : Type*} [Fintype α] (e : α ↪ α) : univ.map e = univ := by
  rw [← e.toEmbedding_equivOfFiniteSelfEmbedding, univ_map_equiv_to_embedding]

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