exists_ne_zero

Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual

URI: https://scilib.ai/kg/mathlib#SeparatingDual.exists_ne_zero

English

For any nonzero x in V, there exists f in the dual such that f(x) ≠ 0.

Русский

Для любого ненулевого вектора x существует функционал f из дуала, такой что f(x) ≠ 0.

LaTeX

$$$\\exists f : StrongDual R V, f(x) \\neq 0$ при x ≠ 0$$

Lean4

theorem exists_ne_zero {x : V} (hx : x ≠ 0) : ∃ f : StrongDual R V, f x ≠ 0 :=
  exists_ne_zero' x hx

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru