def ContinuousMap.realToRCLike {A : Type u_1} (𝕜 : Type u_3) [RCLike 𝕜] [TopologicalSpace A] (f : C(A, ℝ)) : C(A, 𝕜)

Lifting C(A, ℝ) to C(A, 𝕜) using RCLike.ofReal.

Equations

• ContinuousMap.realToRCLike 𝕜 f = { toFun := fun (x : A) => ↑(f x), continuous_toFun := ⋯ }

@[simp]

theorem ContinuousMap.realToRCLike_apply {A : Type u_1} (𝕜 : Type u_3) [RCLike 𝕜] [TopologicalSpace A] (f : C(A, ℝ)) (x : A) : (realToRCLike 𝕜 f) x = ↑(f x)

@[simp]

theorem ContinuousMap.isSelfAdjoint_realToRCLike {A : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [TopologicalSpace A] {f : C(A, ℝ)} : IsSelfAdjoint (realToRCLike 𝕜 f)

@[simp]

theorem ContinuousMap.spectrum_realToRCLike {A : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [TopologicalSpace A] (f : C(A, ℝ)) : spectrum ℝ (realToRCLike 𝕜 f) = spectrum ℝ f

theorem ContinuousMap.monotone_realToRCLike (A : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] [TopologicalSpace A] : Monotone (realToRCLike 𝕜)

def ContinuousMap.rclikeToReal {A : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [TopologicalSpace A] (f : C(A, 𝕜)) : C(A, ℝ)

Mapping C(A, 𝕜) to C(A, ℝ) using RCLike.re.

Equations

• f.rclikeToReal = { toFun := fun (x : A) => RCLike.re (f x), continuous_toFun := ⋯ }

@[simp]

theorem ContinuousMap.rclikeToReal_apply {A : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [TopologicalSpace A] (f : C(A, 𝕜)) (x : A) : f.rclikeToReal x = RCLike.re (f x)

@[simp]

theorem ContinuousMap.rclikeToReal_realToRCLike {A : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [TopologicalSpace A] (f : C(A, ℝ)) : (realToRCLike 𝕜 f).rclikeToReal = f

theorem ContinuousMap.IsSelfAdjoint.realToRCLike_rclikeToReal {A : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [TopologicalSpace A] {f : C(A, 𝕜)} (hf : IsSelfAdjoint f) : realToRCLike 𝕜 f.rclikeToReal = f

theorem ContinuousMap.range_realToRCLike_eq_isSelfAdjoint {A : Type u_1} (𝕜 : Type u_3) [RCLike 𝕜] [TopologicalSpace A] : Set.range (realToRCLike 𝕜) = {f : C(A, 𝕜) | IsSelfAdjoint f}

@[simp]

theorem ContinuousMap.isometry_realToRCLike {A : Type u_1} (𝕜 : Type u_3) [RCLike 𝕜] [TopologicalSpace A] [CompactSpace A] : Isometry (realToRCLike 𝕜)