continuous_linear_map.eval

Stream: Is there code for X?

[Scott Morrison]

variables (𝕜 : Type*) [normed_field 𝕜]
variables (X Y : Type*) [normed_group X] [normed_space 𝕜 X] [normed_group Y] [normed_space 𝕜 Y]
-- TODO surely this is in mathlib?
def continuous_linear_map.eval (x : X) : (X →L[𝕜] Y) →ₗ[𝕜] Y :=
{ to_fun := λ T, T x,
  map_add' := sorry,
  map_smul' := sorry, }

[Patrick Massot]

docs#continuous_linear_map.apply

[Patrick Massot]

You even get E →L[𝕜] (E →L[𝕜] F) →L[𝕜] F (adding linearity with respect to x compared to your wish)

[Moritz Doll]

There is also docs#continuous_linear_map.coe_lm

[Jireh Loreaux]

Do we not have this?

import analysis.normed_space.operator_norm

variables {𝕜 𝕜₂ E F : Type*} [seminormed_add_comm_group E] [seminormed_add_comm_group F]
  [nontrivially_normed_field 𝕜] [nontrivially_normed_field 𝕜₂]
  [normed_space 𝕜 E] [normed_space 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [ring_hom_isometric σ₁₂]

noncomputable def continuous_linear_map.eval (x : E) : (E →SL[σ₁₂] F) →L[𝕜₂] F :=
linear_map.mk_continuous ⟨λ f, f x, λ f g, rfl, λ k f, rfl⟩ (∥x∥)
  (λ f, mul_comm (∥f∥) (∥x∥) ▸ f.le_op_norm x)

[Jireh Loreaux]

Ah, nevermind, it's docs#continuous_linear_map.apply'

[Jireh Loreaux]

Ha! I didn't even realize I was posting in an old thread. :face_palm:

[Kevin Buzzard]

As far as I know it's only recently that one has been able to spot this; now if you start a "new" thread with a title which happens to be the title of an old thread (at least in the app) you get a right-arrow button by the title which lets you jump to the thread without having to post anything in it.

[Johan Commelin]

Pro Tip: Ctrl-. will also do that (-;