exists_eq_one — Mathlib

English

For every nonzero vector x in V there exists a continuous linear functional f (in the separating dual) such that f(x) = 1.

Русский

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

LaTeX

$$$\exists f \in V^*\quad (f(x) = 1)$$$

Lean4

theorem exists_eq_one {x : V} (hx : x ≠ 0) : ∃ f : StrongDual R V, f x = 1 :=
  by
  rcases exists_ne_zero (R := R) hx with ⟨f, hf⟩
  exact ⟨(f x)⁻¹ • f, inv_mul_cancel₀ hf⟩

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