doubleDualEmb_injective — Mathlib

English

The map doubleDualEmb: α → AddChar (AddChar α ℂ) ℂ is injective.

Русский

Отображение doubleDualEmb: α → AddChar (AddChar α ℂ) ℂ инъективно.

LaTeX

$$$ \text{doubleDualEmb} \;: \alpha \to AddChar(AddChar(\alpha, \mathbb{C}), \mathbb{C}) \text{ is injective} $$$

Lean4

theorem doubleDualEmb_injective : Injective (doubleDualEmb : α → AddChar (AddChar α ℂ) ℂ) :=
  doubleDualEmb.ker_eq_bot_iff.1 <|
    eq_bot_iff.2 fun a ha ↦ forall_apply_eq_zero.1 fun ψ ↦ by simpa using DFunLike.congr_fun ha (Additive.ofMul ψ)

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