toWeakDual_inj — Mathlib

English

There is a canonical linear equivalence between WeakDual and StrongDual given by the identity map.

Русский

Существует каноническое линейное эквивалентное отображение между WeakDual и StrongDual, задаваемое тождественным отображением.

LaTeX

$$$ toWeakDual = id$ on the underlying structure, i.e., $toWeakDual x' = x'$$$

Lean4

@[simp]
theorem toWeakDual_inj (x' y' : StrongDual R M) : toWeakDual x' = toWeakDual y' ↔ x' = y' :=
  (LinearEquiv.injective toWeakDual).eq_iff

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