separatingDual_iff_injective — Mathlib

English

SeparatingDual R V is equivalent to the injectivity of the flipped coeLM map.

Русский

Свойство разделяющего дуала эквивалентно инъективности отображения coeLM с переворачиванием аргументов.

LaTeX

$$$SeparatingDual\\; R\\; V \\iff \\text{Injective} (\\text{ContinuousLinearMap.coeLM}(R) .flip)$$$

Lean4

theorem _root_.separatingDual_iff_injective :
    SeparatingDual R V ↔ Function.Injective (ContinuousLinearMap.coeLM (R := R) R (M := V) (N₃ := R)).flip :=
  by
  simp_rw [separatingDual_def, Ne, injective_iff_map_eq_zero]
  congrm ∀ v, ?_
  rw [not_imp_comm, LinearMap.ext_iff]
  push_neg; rfl

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