Support functional

Stream: Is there code for X?

[Yaël Dillies]

What's the best way to get a functional of prescribed norm?

import analysis.normed_space.operator_norm

variables {E : Type*} [normed_add_comm_group E] [normed_space ℝ E]

lemma exists_norm (x : E) : ∃ g : E →L[ℝ] ℝ, ‖g‖ = 1 ∧ g x = ‖x‖ := sorry

[Moritz Doll]

(deleted)

[Moritz Doll]

(deleted)

[Anatole Dedecker]

This is exactly docs#exists_dual_vector'

[Yaël Dillies]

Ahahah! I knew it had to be around Hahn-Banach, but I was looking for the separation statement.