toContinuousMap — Mathlib

English

There is an embedding of FunSpace into the space of continuous maps: α ↦ α.toContinuousMap.

Русский

Существует вложение пространства FunSpace в пространство непрерывных отображений: α ↦ α.toContinuousMap.

LaTeX

$$Embedding: FunSpace t₀ x₀ r L ↪ C(Icc tmin tmax, E) via α ↦ α.toContinuousMap.$$

Lean4

/-- The embedding of `FunSpace` into the space of continuous maps -/
def toContinuousMap : FunSpace t₀ x₀ r L ↪ C(Icc tmin tmax, E) :=
  ⟨fun α ↦ ⟨α, α.continuous⟩, fun α β h ↦ by cases α; cases β; simpa using h⟩

Похожие утверждения