English
The range of α ↦ α.toContinuousMap is the set of continuous maps φ with Lipschitz constant ≤ L and φ(t0) in the closed ball around x0 of radius r.
Русский
Область значений отображения α ↦ α.toContinuousMap совпадает с множеством непрерывных отображений φ, удовлетворяющих ограничению Липшиця ≤ L и φ(t0) в замкненном шаре вокруг x0 радиуса r.
LaTeX
$$range(λ α:FunSpace t0 x0 r L, α.toContinuousMap) = { φ ∈ C(Icc tmin tmax, E) | LipschitzWith L φ ∧ φ(t0) ∈ closedBall(x0,r) }$$
Lean4
theorem range_toContinuousMap :
range (fun α : FunSpace t₀ x₀ r L ↦ α.toContinuousMap) =
{α : C(Icc tmin tmax, E) | LipschitzWith L α ∧ α t₀ ∈ closedBall x₀ r} :=
by
ext α
constructor
· rintro ⟨⟨α, hα1, hα2⟩, rfl⟩
exact ⟨hα1, hα2⟩
· rintro ⟨hα1, hα2⟩
exact ⟨⟨α, hα1, hα2⟩, rfl⟩
