doubleDualEmb_bijective — Mathlib

English

The double dual embedding is bijective, i.e., the doubleDualEmb is both injective and surjective when α is finite.

Русский

Двойное вложение дуальности является биективным для конечной группы α: оно инъективно и сюръективно.

LaTeX

$$$ \text{doubleDualEmb}: α \to AddChar(AddChar(α, \mathbb{C}), \mathbb{C}) \text{ is bijective} $$$

Lean4

theorem doubleDualEmb_bijective : Bijective (doubleDualEmb : α → AddChar (AddChar α ℂ) ℂ) :=
  by
  cases nonempty_fintype α
  exact (Fintype.bijective_iff_injective_and_card _).2 ⟨doubleDualEmb_injective, card_eq.symm.trans card_eq.symm⟩

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