univ_map_equiv_to_embedding — Mathlib

English

For e : α ≃ β, univ.map e.toEmbedding = univ.

Русский

Для эквивалентности e : α ≃ β, отображение универсума через э (встраивание) даёт универcум.

LaTeX

$$$ univ.map e.toEmbedding = univ $$$

Lean4

theorem univ_map_equiv_to_embedding {α β : Type*} [Fintype α] [Fintype β] (e : α ≃ β) : univ.map e.toEmbedding = univ :=
  eq_univ_iff_forall.mpr fun b => mem_map.mpr ⟨e.symm b, mem_univ _, by simp⟩

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