mathlib documentation

analysis.normed_space.basic

Normed spaces #

In this file we define (semi)normed spaces and algebras. We also prove some theorems about these definitions.

@[class]

structure normed_space (α : Type u_5) (β : Type u_6) [normed_field α] [seminormed_add_comm_group β] :

Type (max u_5 u_6)

to_module : module α β
norm_smul_le : ∀ (a : α) (b : β), ∥a • b∥ ≤ ∥a∥ * ∥b∥

A normed space over a normed field is a vector space endowed with a norm which satisfies the equality ∥c • x∥ = ∥c∥ ∥x∥. We require only ∥c • x∥ ≤ ∥c∥ ∥x∥ in the definition, then prove ∥c • x∥ = ∥c∥ ∥x∥ in norm_smul.

Note that since this requires seminormed_add_comm_group and not normed_add_comm_group, this typeclass can be used for "semi normed spaces" too, just as module can be used for "semi modules".

Instances of this typeclass

Instances of other typeclasses for normed_space

normed_space.has_sizeof_inst

@[protected, instance]

def normed_space.has_bounded_smul {α : Type u_1} {β : Type u_2} [normed_field α] [seminormed_add_comm_group β] [normed_space α β] :

has_bounded_smul α β

@[protected, instance]

def normed_field.to_normed_space {α : Type u_1} [normed_field α] :

normed_space α α

Equations

normed_field.to_normed_space = {to_module := semiring.to_module ring.to_semiring, norm_smul_le := _}

theorem norm_smul {α : Type u_1} {β : Type u_2} [normed_field α] [seminormed_add_comm_group β] [normed_space α β] (s : α) (x : β) :

∥s • x∥ = ∥s∥ * ∥x∥

theorem norm_zsmul {β : Type u_2} [seminormed_add_comm_group β] (α : Type u_1) [normed_field α] [normed_space α β] (n : ℤ) (x : β) :

∥n • x∥ = ∥↑n∥ * ∥x∥

@[simp]

theorem abs_norm_eq_norm {β : Type u_2} [seminormed_add_comm_group β] (z : β) :

|∥z∥| = ∥z∥

theorem inv_norm_smul_mem_closed_unit_ball {β : Type u_2} [seminormed_add_comm_group β] [normed_space ℝ β] (x : β) :

∥x∥⁻¹ • x ∈ metric.closed_ball 0 1

theorem dist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [seminormed_add_comm_group β] [normed_space α β] (s : α) (x y : β) :

has_dist.dist (s • x) (s • y) = ∥s∥ * has_dist.dist x y

theorem nnnorm_smul {α : Type u_1} {β : Type u_2} [normed_field α] [seminormed_add_comm_group β] [normed_space α β] (s : α) (x : β) :

∥s • x∥₊ = ∥s∥₊ * ∥x∥₊

theorem nndist_smul {α : Type u_1} {β : Type u_2} [normed_field α] [seminormed_add_comm_group β] [normed_space α β] (s : α) (x y : β) :

has_nndist.nndist (s • x) (s • y) = ∥s∥₊ * has_nndist.nndist x y

theorem lipschitz_with_smul {α : Type u_1} {β : Type u_2} [normed_field α] [seminormed_add_comm_group β] [normed_space α β] (s : α) :

lipschitz_with ∥s∥₊ (has_smul.smul s)

theorem norm_smul_of_nonneg {β : Type u_2} [seminormed_add_comm_group β] [normed_space ℝ β] {t : ℝ} (ht : 0 ≤ t) (x : β) :

∥t • x∥ = t * ∥x∥

theorem eventually_nhds_norm_smul_sub_lt {α : Type u_1} [normed_field α] {E : Type u_5} [seminormed_add_comm_group E] [normed_space α E] (c : α) (x : E) {ε : ℝ} (h : 0 < ε) :

∀ᶠ (y : E) in nhds x, ∥c • (y - x)∥ < ε

theorem filter.tendsto.zero_smul_is_bounded_under_le {α : Type u_1} {ι : Type u_4} [normed_field α] {E : Type u_5} [seminormed_add_comm_group E] [normed_space α E] {f : ι → α} {g : ι → E} {l : filter ι} (hf : filter.tendsto f l (nhds 0)) (hg : filter.is_bounded_under has_le.le l (has_norm.norm ∘ g)) :

filter.tendsto (λ (x : ι), f x • g x) l (nhds 0)

theorem filter.is_bounded_under.smul_tendsto_zero {α : Type u_1} {ι : Type u_4} [normed_field α] {E : Type u_5} [seminormed_add_comm_group E] [normed_space α E] {f : ι → α} {g : ι → E} {l : filter ι} (hf : filter.is_bounded_under has_le.le l (has_norm.norm ∘ f)) (hg : filter.tendsto g l (nhds 0)) :

filter.tendsto (λ (x : ι), f x • g x) l (nhds 0)

theorem closure_ball {E : Type u_5} [seminormed_add_comm_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :

closure (metric.ball x r) = metric.closed_ball x r

theorem frontier_ball {E : Type u_5} [seminormed_add_comm_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :

frontier (metric.ball x r) = metric.sphere x r

theorem interior_closed_ball {E : Type u_5} [seminormed_add_comm_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :

interior (metric.closed_ball x r) = metric.ball x r

theorem frontier_closed_ball {E : Type u_5} [seminormed_add_comm_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :

frontier (metric.closed_ball x r) = metric.sphere x r

@[protected, instance]

def add_subgroup.zmultiples.discrete_topology {E : Type u_1} [normed_add_comm_group E] [normed_space ℚ E] (e : E) :

discrete_topology ↥(add_subgroup.zmultiples e)

theorem homeomorph_unit_ball_apply_coe {E : Type u_5} [seminormed_add_comm_group E] [normed_space ℝ E] (x : E) :

↑(⇑homeomorph_unit_ball x) = (real.sqrt (1 + ∥x∥ ^ 2))⁻¹ • x

noncomputable def homeomorph_unit_ball {E : Type u_5} [seminormed_add_comm_group E] [normed_space ℝ E] :

E ≃ₜ ↥(metric.ball 0 1)

A (semi) normed real vector space is homeomorphic to the unit ball in the same space. This homeomorphism sends x : E to (1 + ∥x∥²)^(- ½) • x.

In many cases the actual implementation is not important, so we don't mark the projection lemmas homeomorph_unit_ball_apply_coe and homeomorph_unit_ball_symm_apply as @[simp].

See also cont_diff_homeomorph_unit_ball and cont_diff_on_homeomorph_unit_ball_symm for smoothness properties that hold when E is an inner-product space.

Equations

homeomorph_unit_ball = {to_equiv := {to_fun := λ (x : E), ⟨(real.sqrt (1 + ∥x∥ ^ 2))⁻¹ • x, _⟩, inv_fun := λ (y : ↥(metric.ball 0 1)), (real.sqrt (1 - ∥↑y∥ ^ 2))⁻¹ • ↑y, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}

theorem homeomorph_unit_ball_symm_apply {E : Type u_5} [seminormed_add_comm_group E] [normed_space ℝ E] (y : ↥(metric.ball 0 1)) :

⇑(homeomorph_unit_ball.symm) y = (real.sqrt (1 - ∥↑y∥ ^ 2))⁻¹ • ↑y

@[simp]

theorem coe_homeomorph_unit_ball_apply_zero {E : Type u_5} [seminormed_add_comm_group E] [normed_space ℝ E] :

↑(⇑homeomorph_unit_ball 0) = 0

@[protected, instance]

def ulift.normed_space {α : Type u_1} [normed_field α] {E : Type u_5} [seminormed_add_comm_group E] [normed_space α E] :

normed_space α (ulift E)

Equations

ulift.normed_space = {to_module := {to_distrib_mul_action := module.to_distrib_mul_action ulift.module', add_smul := _, zero_smul := _}, norm_smul_le := _}

@[protected, instance]

def prod.normed_space {α : Type u_1} [normed_field α] {E : Type u_5} [seminormed_add_comm_group E] [normed_space α E] {F : Type u_6} [seminormed_add_comm_group F] [normed_space α F] :

normed_space α (E × F)

The product of two normed spaces is a normed space, with the sup norm.

Equations

prod.normed_space = {to_module := {to_distrib_mul_action := module.to_distrib_mul_action prod.module, add_smul := _, zero_smul := _}, norm_smul_le := _}

@[protected, instance]

def pi.normed_space {α : Type u_1} {ι : Type u_4} [normed_field α] {E : ι → Type u_2} [fintype ι] [Π (i : ι), seminormed_add_comm_group (E i)] [Π (i : ι), normed_space α (E i)] :

normed_space α (Π (i : ι), E i)

The product of finitely many normed spaces is a normed space, with the sup norm.

Equations

pi.normed_space = {to_module := pi.module ι (λ (i : ι), E i) α (λ (i : ι), normed_space.to_module), norm_smul_le := _}

@[protected, instance]

def submodule.normed_space {𝕜 : Type u_1} {R : Type u_2} [has_smul 𝕜 R] [normed_field 𝕜] [ring R] {E : Type u_3} [seminormed_add_comm_group E] [normed_space 𝕜 E] [module R E] [is_scalar_tower 𝕜 R E] (s : submodule R E) :

normed_space 𝕜 ↥s

A subspace of a normed space is also a normed space, with the restriction of the norm.

Equations

s.normed_space = {to_module := s.module' _inst_13, norm_smul_le := _}

theorem rescale_to_shell_semi_normed {α : Type u_1} [normed_field α] {E : Type u_5} [seminormed_add_comm_group E] [normed_space α E] {c : α} (hc : 1 < ∥c∥) {ε : ℝ} (εpos : 0 < ε) {x : E} (hx : ∥x∥ ≠ 0) :

∃ (d : α), d ≠ 0 ∧ ∥d • x∥ < ε ∧ ε / ∥c∥ ≤ ∥d • x∥ ∧ ∥d∥⁻¹ ≤ ε⁻¹ * ∥c∥ * ∥x∥

If there is a scalar c with ∥c∥>1, then any element with nonzero norm can be moved by scalar multiplication to any shell of width ∥c∥. Also recap information on the norm of the rescaling element that shows up in applications.

@[protected, instance]

def normed_space.to_module' {α : Type u_1} [normed_field α] {F : Type u_6} [normed_add_comm_group F] [normed_space α F] :

While this may appear identical to normed_space.to_module, it contains an implicit argument involving normed_add_comm_group.to_seminormed_add_comm_group that typeclass inference has trouble inferring.

Specifically, the following instance cannot be found without this normed_space.to_module':

example
  (𝕜 ι : Type*) (E : ι → Type*)
  [normed_field 𝕜] [Π i, normed_add_comm_group (E i)] [Π i, normed_space 𝕜 (E i)] :
  Π i, module 𝕜 (E i) := by apply_instance

This Zulip thread gives some more context.

Equations

normed_space.to_module' = normed_space.to_module

theorem exists_norm_eq (E : Type u_5) [normed_add_comm_group E] [normed_space ℝ E] [nontrivial E] {c : ℝ} (hc : 0 ≤ c) :

∃ (x : E), ∥x∥ = c

@[simp]

theorem range_norm (E : Type u_5) [normed_add_comm_group E] [normed_space ℝ E] [nontrivial E] :

set.range has_norm.norm = set.Ici 0

theorem nnnorm_surjective (E : Type u_5) [normed_add_comm_group E] [normed_space ℝ E] [nontrivial E] :

function.surjective has_nnnorm.nnnorm

@[simp]

theorem range_nnnorm (E : Type u_5) [normed_add_comm_group E] [normed_space ℝ E] [nontrivial E] :

set.range has_nnnorm.nnnorm = set.univ

theorem interior_closed_ball' {E : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [nontrivial E] (x : E) (r : ℝ) :

interior (metric.closed_ball x r) = metric.ball x r

theorem frontier_closed_ball' {E : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [nontrivial E] (x : E) (r : ℝ) :

frontier (metric.closed_ball x r) = metric.sphere x r

theorem rescale_to_shell {α : Type u_1} [normed_field α] {E : Type u_5} [normed_add_comm_group E] [normed_space α E] {c : α} (hc : 1 < ∥c∥) {ε : ℝ} (εpos : 0 < ε) {x : E} (hx : x ≠ 0) :

∃ (d : α), d ≠ 0 ∧ ∥d • x∥ < ε ∧ ε / ∥c∥ ≤ ∥d • x∥ ∧ ∥d∥⁻¹ ≤ ε⁻¹ * ∥c∥ * ∥x∥

If there is a scalar c with ∥c∥>1, then any element can be moved by scalar multiplication to any shell of width ∥c∥. Also recap information on the norm of the rescaling element that shows up in applications.

theorem normed_space.exists_lt_norm (𝕜 : Type u_5) (E : Type u_6) [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [nontrivial E] (c : ℝ) :

∃ (x : E), c < ∥x∥

If E is a nontrivial normed space over a nontrivially normed field 𝕜, then E is unbounded: for any c : ℝ, there exists a vector x : E with norm strictly greater than c.

@[protected]

theorem normed_space.unbounded_univ (𝕜 : Type u_5) (E : Type u_6) [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [nontrivial E] :

¬metric.bounded set.univ

@[protected]

theorem normed_space.noncompact_space (𝕜 : Type u_5) (E : Type u_6) [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [nontrivial E] :

noncompact_space E

A normed vector space over a nontrivially normed field is a noncompact space. This cannot be an instance because in order to apply it, Lean would have to search for normed_space 𝕜 E with unknown 𝕜. We register this as an instance in two cases: 𝕜 = E and 𝕜 = ℝ.

@[protected, instance]

def nontrivially_normed_field.noncompact_space (𝕜 : Type u_5) [nontrivially_normed_field 𝕜] :

noncompact_space 𝕜

@[protected, instance]

def real_normed_space.noncompact_space (E : Type u_6) [normed_add_comm_group E] [nontrivial E] [normed_space ℝ E] :

noncompact_space E

@[class]

structure normed_algebra (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] :

Type (max u_5 u_6)

to_algebra : algebra 𝕜 𝕜'
norm_smul_le : ∀ (r : 𝕜) (x : 𝕜'), ∥r • x∥ ≤ ∥r∥ * ∥x∥

A normed algebra 𝕜' over 𝕜 is normed module that is also an algebra.

See the implementation notes for algebra for a discussion about non-unital algebras. Following the strategy there, a non-unital normed algebra can be written as:

variables [normed_field 𝕜] [non_unital_semi_normed_ring 𝕜']
variables [normed_module 𝕜 𝕜'] [smul_comm_class 𝕜 𝕜' 𝕜'] [is_scalar_tower 𝕜 𝕜' 𝕜']

Instances of this typeclass

Instances of other typeclasses for normed_algebra

normed_algebra.has_sizeof_inst

@[protected, instance]

def normed_algebra.to_normed_space {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :

normed_space 𝕜 𝕜'

Equations

normed_algebra.to_normed_space 𝕜' = {to_module := algebra.to_module normed_algebra.to_algebra, norm_smul_le := _}

@[protected, instance]

def normed_algebra.to_normed_space' {𝕜 : Type u_5} [normed_field 𝕜] {𝕜' : Type u_1} [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :

normed_space 𝕜 𝕜'

While this may appear identical to normed_algebra.to_normed_space, it contains an implicit argument involving normed_ring.to_semi_normed_ring that typeclass inference has trouble inferring.

Specifically, the following instance cannot be found without this normed_space.to_module':

example
  (𝕜 ι : Type*) (E : ι → Type*)
  [normed_field 𝕜] [Π i, normed_ring (E i)] [Π i, normed_algebra 𝕜 (E i)] :
  Π i, module 𝕜 (E i) := by apply_instance

See normed_space.to_module' for a similar situation.

Equations

normed_algebra.to_normed_space' = normed_algebra.to_normed_space 𝕜'

theorem norm_algebra_map {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] (x : 𝕜) :

∥⇑(algebra_map 𝕜 𝕜') x∥ = ∥x∥ * ∥1∥

theorem nnnorm_algebra_map {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] (x : 𝕜) :

∥⇑(algebra_map 𝕜 𝕜') x∥₊ = ∥x∥₊ * ∥1∥₊

@[simp]

theorem norm_algebra_map' {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] [norm_one_class 𝕜'] (x : 𝕜) :

∥⇑(algebra_map 𝕜 𝕜') x∥ = ∥x∥

@[simp]

theorem nnnorm_algebra_map' {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] [norm_one_class 𝕜'] (x : 𝕜) :

∥⇑(algebra_map 𝕜 𝕜') x∥₊ = ∥x∥₊

@[simp]

theorem norm_algebra_map_nnreal (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [norm_one_class 𝕜'] [normed_algebra ℝ 𝕜'] (x : nnreal) :

∥⇑(algebra_map nnreal 𝕜') x∥ = ↑x

@[simp]

theorem nnnorm_algebra_map_nnreal (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [norm_one_class 𝕜'] [normed_algebra ℝ 𝕜'] (x : nnreal) :

∥⇑(algebra_map nnreal 𝕜') x∥₊ = x

theorem algebra_map_isometry (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] [norm_one_class 𝕜'] :

isometry ⇑(algebra_map 𝕜 𝕜')

In a normed algebra, the inclusion of the base field in the extended field is an isometry.

@[protected, instance]

def normed_algebra.id (𝕜 : Type u_5) [normed_field 𝕜] :

normed_algebra 𝕜 𝕜

Equations

normed_algebra.id 𝕜 = {to_algebra := {to_has_smul := mul_action.to_has_smul distrib_mul_action.to_mul_action, to_ring_hom := algebra.to_ring_hom (algebra.id 𝕜), commutes' := _, smul_def' := _}, norm_smul_le := _}

@[protected, instance]

def normed_algebra_rat {𝕜 : Type u_1} [normed_division_ring 𝕜] [char_zero 𝕜] [normed_algebra ℝ 𝕜] :

normed_algebra ℚ 𝕜

Any normed characteristic-zero division ring that is a normed_algebra over the reals is also a normed algebra over the rationals.

Phrased another way, if 𝕜 is a normed algebra over the reals, then algebra_rat respects that norm.

Equations

normed_algebra_rat = {to_algebra := algebra_rat _inst_5, norm_smul_le := _}

@[protected, instance]

def punit.normed_algebra (𝕜 : Type u_5) [normed_field 𝕜] :

normed_algebra 𝕜 punit

Equations

punit.normed_algebra 𝕜 = {to_algebra := punit.algebra (semifield.to_comm_semiring 𝕜), norm_smul_le := _}

@[protected, instance]

def ulift.normed_algebra (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :

normed_algebra 𝕜 (ulift 𝕜')

Equations

ulift.normed_algebra 𝕜 𝕜' = {to_algebra := ulift.algebra normed_algebra.to_algebra, norm_smul_le := _}

@[protected, instance]

def prod.normed_algebra (𝕜 : Type u_5) [normed_field 𝕜] {E : Type u_1} {F : Type u_2} [semi_normed_ring E] [semi_normed_ring F] [normed_algebra 𝕜 E] [normed_algebra 𝕜 F] :

normed_algebra 𝕜 (E × F)

The product of two normed algebras is a normed algebra, with the sup norm.

Equations

prod.normed_algebra 𝕜 = {to_algebra := prod.algebra 𝕜 E F normed_algebra.to_algebra, norm_smul_le := _}

@[protected, instance]

def pi.normed_algebra {ι : Type u_4} (𝕜 : Type u_5) [normed_field 𝕜] {E : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_ring (E i)] [Π (i : ι), normed_algebra 𝕜 (E i)] :

normed_algebra 𝕜 (Π (i : ι), E i)

The product of finitely many normed algebras is a normed algebra, with the sup norm.

Equations

pi.normed_algebra 𝕜 = {to_algebra := {to_has_smul := mul_action.to_has_smul distrib_mul_action.to_mul_action, to_ring_hom := algebra.to_ring_hom (pi.algebra ι E), commutes' := _, smul_def' := _}, norm_smul_le := _}

@[protected, instance]

def restrict_scalars.seminormed_add_comm_group {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : seminormed_add_comm_group E] :

seminormed_add_comm_group (restrict_scalars 𝕜 𝕜' E)

Equations

restrict_scalars.seminormed_add_comm_group = I

@[protected, instance]

def restrict_scalars.normed_add_comm_group {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [I : normed_add_comm_group E] :

normed_add_comm_group (restrict_scalars 𝕜 𝕜' E)

Equations

restrict_scalars.normed_add_comm_group = I

@[protected, instance]

def restrict_scalars.normed_space (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] (E : Type u_7) [seminormed_add_comm_group E] [normed_space 𝕜' E] :

normed_space 𝕜 (restrict_scalars 𝕜 𝕜' E)

If E is a normed space over 𝕜' and 𝕜 is a normed algebra over 𝕜', then restrict_scalars.module is additionally a normed_space.

Equations

restrict_scalars.normed_space 𝕜 𝕜' E = {to_module := {to_distrib_mul_action := module.to_distrib_mul_action (restrict_scalars.module 𝕜 𝕜' E), add_smul := _, zero_smul := _}, norm_smul_le := _}

def module.restrict_scalars.normed_space_orig {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [normed_field 𝕜'] [seminormed_add_comm_group E] [I : normed_space 𝕜' E] :

normed_space 𝕜' (restrict_scalars 𝕜 𝕜' E)

The action of the original normed_field on restrict_scalars 𝕜 𝕜' E. This is not an instance as it would be contrary to the purpose of restrict_scalars.

Equations

module.restrict_scalars.normed_space_orig = I

def normed_space.restrict_scalars (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] (E : Type u_7) [seminormed_add_comm_group E] [normed_space 𝕜' E] :

normed_space 𝕜 E

Warning: This declaration should be used judiciously. Please consider using is_scalar_tower and/or restrict_scalars 𝕜 𝕜' E instead.

This definition allows the restrict_scalars.normed_space instance to be put directly on E rather on restrict_scalars 𝕜 𝕜' E. This would be a very bad instance; both because 𝕜' cannot be inferred, and because it is likely to create instance diamonds.

Equations

normed_space.restrict_scalars 𝕜 𝕜' E = restrict_scalars.normed_space 𝕜 𝕜' E