exists_separating_of_ne — Mathlib

English

SeparatingDual R V is equivalent to the injectivity of the flip of ContinuousLinearMap.coeLM.

Русский

Разделяющее дуальное свойство эквивалентно инъективности отображения, сопряжённого с ContinuousLinearMap.coeLM.

LaTeX

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

Lean4

theorem exists_separating_of_ne {x y : V} (h : x ≠ y) : ∃ f : StrongDual R V, f x ≠ f y :=
  by
  rcases exists_ne_zero (R := R) (sub_ne_zero_of_ne h) with ⟨f, hf⟩
  exact ⟨f, by simpa [sub_ne_zero] using hf⟩

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