mathlib documentation

analysis.normed_space.basic

Normed spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
@[class]
structure normed_space (α : Type u_5) (β : Type u_6) [normed_field α] [seminormed_add_comm_group β] :
Type (max u_5 u_6)

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
source
@[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 α β
source
@[protected, instance]
def real.module  :
module ℝ ℝ
Equations
source
@[protected, instance]
def normed_field.to_normed_space {α : Type u_1} [normed_field α] :
normed_space α α
Equations
source
@[protected, instance]
def normed_field.to_has_bounded_smul {α : Type u_1} [normed_field α] :
has_bounded_smul α α
source
theorem norm_zsmul {β : Type u_2} [seminormed_add_comm_group β] (α : Type u_1) [normed_field α] [normed_space α β] (n : ℤ) (x : β) :
‖n • x‖ = ‖↑n‖ * ‖x‖
source
@[simp]
theorem abs_norm {β : Type u_2} [seminormed_add_comm_group β] (z : β) :
|‖z‖| = ‖z‖
source
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
source
theorem norm_smul_of_nonneg {β : Type u_2} [seminormed_add_comm_group β] [normed_space ℝ β] {t : ℝ} (ht : 0 ≤ t) (x : β) :
‖t • x‖ = t * ‖x‖
source
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)‖ < ε
source
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)
source
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)
source
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
source
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
source
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
source
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
source
theorem interior_sphere {E : Type u_5} [seminormed_add_comm_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :
interior (metric.sphere x r) = ∅
source
theorem frontier_sphere {E : Type u_5} [seminormed_add_comm_group E] [normed_space ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :
frontier (metric.sphere x r) = metric.sphere x r
source
@[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)
source
theorem homeomorph_unit_ball_apply_coe {E : Type u_5} [seminormed_add_comm_group E] [normed_space ℝ E] (x : E) :
↑(⇑homeomorph_unit_ball x) = (√ (1 + ‖x‖ ^ 2))⁻¹ • x
source
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
source
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 = (√ (1 - ‖↑y‖ ^ 2))⁻¹ • ↑y
source
@[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
source
@[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
source
@[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
source
@[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
source
@[protected, instance]
def mul_opposite.normed_space {α : Type u_1} [normed_field α] {E : Type u_5} [seminormed_add_comm_group E] [normed_space α E] :
normed_space α Eᵐᵒᵖ
Equations
source
@[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
source
theorem rescale_to_shell_semi_normed_zpow {α : 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) :
∃ (n : ℤ), c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ ε / ‖c‖ ≤ ‖c ^ n • x‖ ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖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.

source
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.

source
@[reducible]
def normed_space.induced {F : Type u_1} (α : Type u_2) (β : Type u_3) (γ : Type u_4) [normed_field α] [add_comm_group β] [module α β] [seminormed_add_comm_group γ] [normed_space α γ] [linear_map_class F α β γ] (f : F) :
normed_space α β

A linear map from a module to a normed_space induces a normed_space structure on the domain, using the seminormed_add_comm_group.induced norm.

See note [reducible non-instances]

Equations
source
@[protected, instance]
def normed_space.to_module' {α : Type u_1} [normed_field α] {F : Type u_6} [normed_add_comm_group F] [normed_space α F] :
module α 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
source
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
source
@[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
source
theorem nnnorm_surjective (E : Type u_5) [normed_add_comm_group E] [normed_space ℝ E] [nontrivial E] :
function.surjective has_nnnorm.nnnorm
source
@[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
source
@[protected, instance]
def real.punctured_nhds_module_ne_bot {E : Type u_1} [add_comm_group E] [topological_space E] [has_continuous_add E] [nontrivial E] [module ℝ E] [has_continuous_smul ℝ E] (x : E) :
(nhds_within x {x}ᶜ).ne_bot

If E is a nontrivial topological module over ℝ, then E has no isolated points. This is a particular case of module.punctured_nhds_ne_bot.

source
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
source
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
source
@[simp]
theorem interior_sphere' {E : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [nontrivial E] (x : E) (r : ℝ) :
interior (metric.sphere x r) = ∅
source
@[simp]
theorem frontier_sphere' {E : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [nontrivial E] (x : E) (r : ℝ) :
frontier (metric.sphere x r) = metric.sphere x r
source
theorem rescale_to_shell_zpow {α : 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) :
∃ (n : ℤ), c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ ε / ‖c‖ ≤ ‖c ^ n • x‖ ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖
source
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.

source
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.

source
@[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
source
@[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 𝕜 = ℝ.

source
@[protected, instance]
def nontrivially_normed_field.noncompact_space (𝕜 : Type u_5) [nontrivially_normed_field 𝕜] :
noncompact_space 𝕜
source
@[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
source
@[class]
structure normed_algebra (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] :
Type (max u_5 u_6)

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
source
@[protected, instance]
def normed_algebra.to_normed_space {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
normed_space 𝕜 𝕜'
Equations
source
@[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
source
theorem norm_algebra_map {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] (x : 𝕜) :
‖⇑(algebra_map 𝕜 𝕜') x‖ = ‖x‖ * ‖1‖
source
theorem nnnorm_algebra_map {𝕜 : Type u_5} (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] (x : 𝕜) :
‖⇑(algebra_map 𝕜 𝕜') x‖₊ = ‖x‖₊ * ‖1‖₊
source
@[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‖
source
@[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‖₊
source
@[simp]
theorem norm_algebra_map_nnreal (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [norm_one_class 𝕜'] [normed_algebra ℝ 𝕜'] (x : nnreal) :
‖⇑(algebra_map nnreal 𝕜') x‖ = ↑x
source
@[simp]
theorem nnnorm_algebra_map_nnreal (𝕜' : Type u_6) [semi_normed_ring 𝕜'] [norm_one_class 𝕜'] [normed_algebra ℝ 𝕜'] (x : nnreal) :
‖⇑(algebra_map nnreal 𝕜') x‖₊ = x
source
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.

source
@[protected, instance]
def normed_algebra.id (𝕜 : Type u_5) [normed_field 𝕜] :
normed_algebra 𝕜 𝕜
Equations
source
@[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
source
@[protected, instance]
def punit.normed_algebra (𝕜 : Type u_5) [normed_field 𝕜] :
normed_algebra 𝕜 punit
Equations
source
@[protected, instance]
def ulift.normed_algebra (𝕜 : Type u_5) (𝕜' : Type u_6) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
normed_algebra 𝕜 (ulift 𝕜')
Equations
source
@[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
source
@[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
source
@[protected, instance]
def mul_opposite.normed_algebra (𝕜 : Type u_5) [normed_field 𝕜] {E : Type u_1} [semi_normed_ring E] [normed_algebra 𝕜 E] :
normed_algebra 𝕜 Eᵐᵒᵖ
Equations
source
@[reducible]
def normed_algebra.induced {F : Type u_1} (α : Type u_2) (β : Type u_3) (γ : Type u_4) [normed_field α] [ring β] [algebra α β] [semi_normed_ring γ] [normed_algebra α γ] [non_unital_alg_hom_class F α β γ] (f : F) :
normed_algebra α β

A non-unital algebra homomorphism from an algebra to a normed_algebra induces a normed_algebra structure on the domain, using the semi_normed_ring.induced norm.

See note [reducible non-instances]

Equations
source
@[protected, instance]
def subalgebra.to_normed_algebra {𝕜 : Type u_1} {A : Type u_2} [semi_normed_ring A] [normed_field 𝕜] [normed_algebra 𝕜 A] (S : subalgebra 𝕜 A) :
normed_algebra 𝕜 ↥S
Equations
source
@[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
source
@[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
source
@[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
source
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
source
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