Theorems · Definition · functional analysis

ContinuousMap.realToRCLike

{X : Type u_1} → (𝕜 : Type u_2) → [inst : TopologicalSpace X] → [inst_1 : RCLike 𝕜] → C(X, ℝ) → C(X, 𝕜)

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

Defined in

Mathlib.Analysis.RCLike.ContinuousMap

Cited by

18 results in Mathlib

Foundations

Depth 160 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceRCLike