Normed spaces

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

class NormedSpace (α : Type u_5) (β : Type u_6) [NormedField α] [SeminormedAddCommGroup β] extends Module : 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 SeminormedAddCommGroup and not NormedAddCommGroup, this typeclass can be used for "semi normed spaces" too, just as Module can be used for "semi modules".

• smul : α → β → β
• one_smul : ∀ (b : β), 1 • b = b
• mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b
• smul_zero : ∀ (a : α), a • 0 = 0
• smul_add : ∀ (a : α) (x y : β), a • (x + y) = a • x + a • y
• add_smul : ∀ (r s : α) (x : β), (r + s) • x = r • x + s • x
• zero_smul : ∀ (x : β), 0 • x = 0
• 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 SeminormedAddCommGroup and not NormedAddCommGroup, this typeclass can be used for "semi normed spaces" too, just as Module can be used for "semi modules".

instance NormedSpace.boundedSMul {α : Type u_1} {β : Type u_2} [NormedField α] [SeminormedAddCommGroup β] [NormedSpace α β] : BoundedSMul α β

Equations

• (_ : BoundedSMul α β) = (_ : BoundedSMul α β)

instance NormedField.toNormedSpace {α : Type u_1} [NormedField α] : NormedSpace α α

Equations

• NormedField.toNormedSpace = NormedSpace.mk (_ : ∀ (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖)

instance NormedField.to_boundedSMul {α : Type u_1} [NormedField α] : BoundedSMul α α

Equations

• (_ : BoundedSMul α α) = (_ : BoundedSMul α α)

theorem norm_zsmul {β : Type u_2} [SeminormedAddCommGroup β] (α : Type u_5) [NormedField α] [NormedSpace α β] (n : ℤ) (x : β) : ‖n • x‖ = ‖↑n‖ * ‖x‖

theorem eventually_nhds_norm_smul_sub_lt {α : Type u_1} [NormedField α] {E : Type u_5} [SeminormedAddCommGroup E] [NormedSpace α E] (c : α) (x : E) {ε : ℝ} (h : 0 < ε) : ∀ᶠ (y : E) in nhds x, ‖c • (y - x)‖ < ε

theorem Filter.Tendsto.zero_smul_isBoundedUnder_le {α : Type u_1} {ι : Type u_4} [NormedField α] {E : Type u_5} [SeminormedAddCommGroup E] [NormedSpace α E] {f : ι → α} {g : ι → E} {l : Filter ι} (hf : Filter.Tendsto f l (nhds 0)) (hg : Filter.IsBoundedUnder (fun (x x_1 : ℝ) => x ≤ x_1) l (norm ∘ g)) : Filter.Tendsto (fun (x : ι) => f x • g x) l (nhds 0)

theorem Filter.IsBoundedUnder.smul_tendsto_zero {α : Type u_1} {ι : Type u_4} [NormedField α] {E : Type u_5} [SeminormedAddCommGroup E] [NormedSpace α E] {f : ι → α} {g : ι → E} {l : Filter ι} (hf : Filter.IsBoundedUnder (fun (x x_1 : ℝ) => x ≤ x_1) l (norm ∘ f)) (hg : Filter.Tendsto g l (nhds 0)) : Filter.Tendsto (fun (x : ι) => f x • g x) l (nhds 0)

instance NormedSpace.discreteTopology_zmultiples {E : Type u_7} [NormedAddCommGroup E] [NormedSpace ℚ E] (e : E) : DiscreteTopology ↥(AddSubgroup.zmultiples e)

Equations

• (_ : DiscreteTopology ↥(AddSubgroup.zmultiples e)) = (_ : DiscreteTopology ↥(AddSubgroup.zmultiples e))

instance ULift.normedSpace {α : Type u_1} [NormedField α] {E : Type u_5} [SeminormedAddCommGroup E] [NormedSpace α E] : NormedSpace α (ULift.{u_7, u_5} E)

Equations

• ULift.normedSpace = let src := ULift.seminormedAddCommGroup; let src := ULift.module'; NormedSpace.mk (_ : ∀ (s : α) (x : ULift.{u_7, u_5} E), ‖s • x.down‖ ≤ ‖s‖ * ‖x.down‖)

instance Prod.normedSpace {α : Type u_1} [NormedField α] {E : Type u_5} [SeminormedAddCommGroup E] [NormedSpace α E] {F : Type u_6} [SeminormedAddCommGroup F] [NormedSpace α F] : NormedSpace α (E × F)

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

Equations

• Prod.normedSpace = let src := Prod.seminormedAddCommGroup; let src := Prod.instModule; NormedSpace.mk (_ : ∀ (s : α) (x : E × F), ‖s • x‖ ≤ ‖s‖ * max ‖x.1‖ ‖x.2‖)

instance Pi.normedSpace {α : Type u_1} {ι : Type u_4} [NormedField α] {E : ι → Type u_7} [Fintype ι] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace α (E i)] : NormedSpace α ((i : ι) → E i)

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

Equations

• Pi.normedSpace = NormedSpace.mk (_ : ∀ (a : α) (f : (i : ι) → E i), ‖a • f‖ ≤ ‖a‖ * ‖f‖)

instance MulOpposite.normedSpace {α : Type u_1} [NormedField α] {E : Type u_5} [SeminormedAddCommGroup E] [NormedSpace α E] : NormedSpace α Eᵐᵒᵖ

Equations

• One or more equations did not get rendered due to their size.

instance Submodule.normedSpace {𝕜 : Type u_7} {R : Type u_8} [SMul 𝕜 R] [NormedField 𝕜] [Ring R] {E : Type u_9} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [Module R E] [IsScalarTower 𝕜 R E] (s : Submodule R E) : NormedSpace 𝕜 ↥s

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

Equations

• Submodule.normedSpace s = NormedSpace.mk (_ : ∀ (c : 𝕜) (x : ↥s), ‖c • ↑x‖ ≤ ‖c‖ * ‖↑x‖)

@[reducible]

def NormedSpace.induced {F : Type u_5} (α : Type u_6) (β : Type u_7) (γ : Type u_8) [NormedField α] [AddCommGroup β] [Module α β] [SeminormedAddCommGroup γ] [NormedSpace α γ] [FunLike F β γ] [LinearMapClass F α β γ] (f : F) : NormedSpace α β

A linear map from a Module to a NormedSpace induces a NormedSpace structure on the domain, using the SeminormedAddCommGroup.induced norm.

See note [reducible non-instances]

Equations

• NormedSpace.induced α β γ f = NormedSpace.mk (_ : ∀ (a : α) (b : β), ‖f (a • b)‖ ≤ ‖a‖ * ‖f b‖)

instance NormedSpace.toModule' {α : Type u_1} [NormedField α] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace α F] : Module α F

While this may appear identical to NormedSpace.toModule, it contains an implicit argument involving NormedAddCommGroup.toSeminormedAddCommGroup that typeclass inference has trouble inferring.

Specifically, the following instance cannot be found without this NormedSpace.toModule':

example
  (𝕜 ι : Type*) (E : ι → Type*)
  [NormedField 𝕜] [Π i, NormedAddCommGroup (E i)] [Π i, NormedSpace 𝕜 (E i)] :
  Π i, Module 𝕜 (E i) := by infer_instance

This Zulip thread gives some more context.

Equations

• NormedSpace.toModule' = NormedSpace.toModule

theorem NormedSpace.exists_lt_norm (𝕜 : Type u_5) (E : Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 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.

theorem NormedSpace.unbounded_univ (𝕜 : Type u_5) (E : Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [Nontrivial E] : ¬Bornology.IsBounded Set.univ

theorem NormedSpace.cobounded_neBot (𝕜 : Type u_5) (E : Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [Nontrivial E] : Filter.NeBot (Bornology.cobounded E)

instance NontriviallyNormedField.cobounded_neBot (𝕜 : Type u_5) [NontriviallyNormedField 𝕜] : Filter.NeBot (Bornology.cobounded 𝕜)

Equations

• (_ : Filter.NeBot (Bornology.cobounded 𝕜)) = (_ : Filter.NeBot (Bornology.cobounded 𝕜))

instance RealNormedSpace.cobounded_neBot (E : Type u_6) [NormedAddCommGroup E] [Nontrivial E] [NormedSpace ℝ E] : Filter.NeBot (Bornology.cobounded E)

Equations

• (_ : Filter.NeBot (Bornology.cobounded E)) = (_ : Filter.NeBot (Bornology.cobounded E))

instance NontriviallyNormedField.infinite (𝕜 : Type u_5) [NontriviallyNormedField 𝕜] : Infinite 𝕜

Equations

• (_ : Infinite 𝕜) = (_ : Infinite 𝕜)

theorem NormedSpace.noncompactSpace (𝕜 : Type u_5) (E : Type u_6) [NormedField 𝕜] [Infinite 𝕜] [NormedAddCommGroup E] [Nontrivial E] [NormedSpace 𝕜 E] : NoncompactSpace E

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

instance NormedField.noncompactSpace (𝕜 : Type u_5) [NormedField 𝕜] [Infinite 𝕜] : NoncompactSpace 𝕜

Equations

• (_ : NoncompactSpace 𝕜) = (_ : NoncompactSpace 𝕜)

instance RealNormedSpace.noncompactSpace (E : Type u_6) [NormedAddCommGroup E] [Nontrivial E] [NormedSpace ℝ E] : NoncompactSpace E

Equations

• (_ : NoncompactSpace E) = (_ : NoncompactSpace E)

class NormedAlgebra (𝕜 : Type u_5) (𝕜' : Type u_6) [NormedField 𝕜] [SeminormedRing 𝕜'] extends Algebra : 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 [NormedField 𝕜] [NonUnitalSeminormedRing 𝕜']
variables [NormedSpace 𝕜 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜']

• smul : 𝕜 → 𝕜' → 𝕜'
• toFun : 𝕜 → 𝕜'
• map_one' : (↑↑Algebra.toRingHom).toFun 1 = 1
• map_mul' : ∀ (x y : 𝕜), (↑↑Algebra.toRingHom).toFun (x * y) = (↑↑Algebra.toRingHom).toFun x * (↑↑Algebra.toRingHom).toFun y
• map_zero' : (↑↑Algebra.toRingHom).toFun 0 = 0
• map_add' : ∀ (x y : 𝕜), (↑↑Algebra.toRingHom).toFun (x + y) = (↑↑Algebra.toRingHom).toFun x + (↑↑Algebra.toRingHom).toFun y
• commutes' : ∀ (r : 𝕜) (x : 𝕜'), Algebra.toRingHom r * x = x * Algebra.toRingHom r
• smul_def' : ∀ (r : 𝕜) (x : 𝕜'), r • x = Algebra.toRingHom r * x
• 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 [NormedField 𝕜] [NonUnitalSeminormedRing 𝕜']
  variables [NormedSpace 𝕜 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜']
  

instance NormedAlgebra.toNormedSpace {𝕜 : Type u_5} (𝕜' : Type u_6) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] : NormedSpace 𝕜 𝕜'

Equations

• NormedAlgebra.toNormedSpace 𝕜' = let src := Algebra.toModule; NormedSpace.mk (_ : ∀ (r : 𝕜) (x : 𝕜'), ‖r • x‖ ≤ ‖r‖ * ‖x‖)

instance NormedAlgebra.toNormedSpace' {𝕜 : Type u_5} [NormedField 𝕜] {𝕜' : Type u_7} [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] : NormedSpace 𝕜 𝕜'

While this may appear identical to NormedAlgebra.toNormedSpace, it contains an implicit argument involving NormedRing.toSeminormedRing that typeclass inference has trouble inferring.

Specifically, the following instance cannot be found without this NormedSpace.toModule':

example
  (𝕜 ι : Type*) (E : ι → Type*)
  [NormedField 𝕜] [Π i, NormedRing (E i)] [Π i, NormedAlgebra 𝕜 (E i)] :
  Π i, Module 𝕜 (E i) := by infer_instance

See NormedSpace.toModule' for a similar situation.

Equations

• NormedAlgebra.toNormedSpace' = inferInstance

theorem norm_algebraMap {𝕜 : Type u_5} (𝕜' : Type u_6) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] (x : 𝕜) : ‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖ * ‖1‖

theorem nnnorm_algebraMap {𝕜 : Type u_5} (𝕜' : Type u_6) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] (x : 𝕜) : ‖(algebraMap 𝕜 𝕜') x‖₊ = ‖x‖₊ * ‖1‖₊

@[simp]

theorem norm_algebraMap' {𝕜 : Type u_5} (𝕜' : Type u_6) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] (x : 𝕜) : ‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖

@[simp]

theorem nnnorm_algebraMap' {𝕜 : Type u_5} (𝕜' : Type u_6) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] (x : 𝕜) : ‖(algebraMap 𝕜 𝕜') x‖₊ = ‖x‖₊

@[simp]

theorem norm_algebraMap_nnreal (𝕜' : Type u_6) [SeminormedRing 𝕜'] [NormOneClass 𝕜'] [NormedAlgebra ℝ 𝕜'] (x : NNReal) : ‖(algebraMap NNReal 𝕜') x‖ = ↑x

@[simp]

theorem nnnorm_algebraMap_nnreal (𝕜' : Type u_6) [SeminormedRing 𝕜'] [NormOneClass 𝕜'] [NormedAlgebra ℝ 𝕜'] (x : NNReal) : ‖(algebraMap NNReal 𝕜') x‖₊ = x

theorem algebraMap_isometry (𝕜 : Type u_5) (𝕜' : Type u_6) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] : Isometry ⇑(algebraMap 𝕜 𝕜')

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

instance NormedAlgebra.id (𝕜 : Type u_5) [NormedField 𝕜] : NormedAlgebra 𝕜 𝕜

Equations

• NormedAlgebra.id 𝕜 = let src := NormedField.toNormedSpace; let src_1 := Algebra.id 𝕜; NormedAlgebra.mk (_ : ∀ (a b : 𝕜), ‖a • b‖ ≤ ‖a‖ * ‖b‖)

instance normedAlgebraRat {𝕜 : Type u_7} [NormedDivisionRing 𝕜] [CharZero 𝕜] [NormedAlgebra ℝ 𝕜] : NormedAlgebra ℚ 𝕜

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 AlgebraRat respects that norm.

Equations

• normedAlgebraRat = NormedAlgebra.mk (_ : ∀ (q : ℚ) (x : 𝕜), ‖q • x‖ ≤ ‖q‖ * ‖x‖)

instance PUnit.normedAlgebra (𝕜 : Type u_5) [NormedField 𝕜] : NormedAlgebra 𝕜 PUnit.{u_7 + 1}

Equations

• PUnit.normedAlgebra 𝕜 = NormedAlgebra.mk (_ : ∀ (q : 𝕜), PUnit.{u_7 + 1} → 0 ≤ ‖q‖ * 0)

instance instNormedAlgebraULiftSeminormedRing (𝕜 : Type u_5) (𝕜' : Type u_6) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] : NormedAlgebra 𝕜 (ULift.{u_7, u_6} 𝕜')

Equations

• instNormedAlgebraULiftSeminormedRing 𝕜 𝕜' = let src := ULift.normedSpace; let src_1 := ULift.algebra; NormedAlgebra.mk (_ : ∀ (a : 𝕜) (b : ULift.{u_7, u_6} 𝕜'), ‖a • b‖ ≤ ‖a‖ * ‖b‖)

instance Prod.normedAlgebra (𝕜 : Type u_5) [NormedField 𝕜] {E : Type u_7} {F : Type u_8} [SeminormedRing E] [SeminormedRing F] [NormedAlgebra 𝕜 E] [NormedAlgebra 𝕜 F] : NormedAlgebra 𝕜 (E × F)

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

Equations

• Prod.normedAlgebra 𝕜 = let src := Prod.normedSpace; let src_1 := Prod.algebra 𝕜 E F; NormedAlgebra.mk (_ : ∀ (a : 𝕜) (b : E × F), ‖a • b‖ ≤ ‖a‖ * ‖b‖)

instance Pi.normedAlgebra {ι : Type u_4} (𝕜 : Type u_5) [NormedField 𝕜] {E : ι → Type u_7} [Fintype ι] [(i : ι) → SeminormedRing (E i)] [(i : ι) → NormedAlgebra 𝕜 (E i)] : NormedAlgebra 𝕜 ((i : ι) → E i)

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

Equations

• Pi.normedAlgebra 𝕜 = let src := Pi.normedSpace; let src_1 := Pi.algebra ι E; NormedAlgebra.mk (_ : ∀ (a : 𝕜) (b : (i : ι) → E i), ‖a • b‖ ≤ ‖a‖ * ‖b‖)

instance MulOpposite.normedAlgebra (𝕜 : Type u_5) [NormedField 𝕜] {E : Type u_8} [SeminormedRing E] [NormedAlgebra 𝕜 E] : NormedAlgebra 𝕜 Eᵐᵒᵖ

Equations

• MulOpposite.normedAlgebra 𝕜 = let src := MulOpposite.normedSpace; let src_1 := MulOpposite.MulOpposite.instAlgebra; NormedAlgebra.mk (_ : ∀ (a : 𝕜) (b : Eᵐᵒᵖ), ‖a • b‖ ≤ ‖a‖ * ‖b‖)

@[reducible]

def NormedAlgebra.induced {F : Type u_5} (α : Type u_6) (β : Type u_7) (γ : Type u_8) [NormedField α] [Ring β] [Algebra α β] [SeminormedRing γ] [NormedAlgebra α γ] [FunLike F β γ] [NonUnitalAlgHomClass F α β γ] (f : F) : NormedAlgebra α β

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

See note [reducible non-instances]

Equations

• NormedAlgebra.induced α β γ f = NormedAlgebra.mk (_ : ∀ (a : α) (b : β), ‖f (a • b)‖ ≤ ‖a‖ * ‖f b‖)

instance Subalgebra.toNormedAlgebra {𝕜 : Type u_5} {A : Type u_6} [SeminormedRing A] [NormedField 𝕜] [NormedAlgebra 𝕜 A] (S : Subalgebra 𝕜 A) : NormedAlgebra 𝕜 ↥S

Equations

• Subalgebra.toNormedAlgebra S = NormedAlgebra.induced 𝕜 (↥S) A (Subalgebra.val S)

instance instSeminormedAddCommGroupRestrictScalars {𝕜 : Type u_8} {𝕜' : Type u_9} {E : Type u_10} [I : SeminormedAddCommGroup E] : SeminormedAddCommGroup (RestrictScalars 𝕜 𝕜' E)

Equations

• instSeminormedAddCommGroupRestrictScalars = I

instance instNormedAddCommGroupRestrictScalars {𝕜 : Type u_8} {𝕜' : Type u_9} {E : Type u_10} [I : NormedAddCommGroup E] : NormedAddCommGroup (RestrictScalars 𝕜 𝕜' E)

Equations

• instNormedAddCommGroupRestrictScalars = I

instance RestrictScalars.normedSpace (𝕜 : Type u_5) (𝕜' : Type u_6) [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] (E : Type u_7) [SeminormedAddCommGroup E] [NormedSpace 𝕜' E] : NormedSpace 𝕜 (RestrictScalars 𝕜 𝕜' E)

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

Equations

• RestrictScalars.normedSpace 𝕜 𝕜' E = let src := RestrictScalars.module 𝕜 𝕜' E; NormedSpace.mk (_ : ∀ (c : 𝕜) (x : RestrictScalars 𝕜 𝕜' E), ‖(algebraMap 𝕜 𝕜') c • x‖ ≤ ‖c‖ * ‖x‖)

def Module.RestrictScalars.normedSpaceOrig {𝕜 : Type u_8} {𝕜' : Type u_9} {E : Type u_10} [NormedField 𝕜'] [SeminormedAddCommGroup E] [I : NormedSpace 𝕜' E] : NormedSpace 𝕜' (RestrictScalars 𝕜 𝕜' E)

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

Equations

• Module.RestrictScalars.normedSpaceOrig = I

def NormedSpace.restrictScalars (𝕜 : Type u_5) (𝕜' : Type u_6) [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] (E : Type u_7) [SeminormedAddCommGroup E] [NormedSpace 𝕜' E] : NormedSpace 𝕜 E

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

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

Equations

• NormedSpace.restrictScalars 𝕜 𝕜' E = RestrictScalars.normedSpace 𝕜 𝕜' E