isUniformInducing_toContinuousMap

Mathlib.Analysis.ODE.PicardLindelof

URI: https://scilib.ai/kg/mathlib#ODE.FunSpace.isUniformInducing_toContinuousMap

English

If E is a complete space, then FunSpace t0 x0 r L is complete.

Русский

Если E — полное пространство, то FunSpace t0 x0 r L также полное.

LaTeX

$$CompleteSpace(FunSpace t0 x0 r L)$$

Lean4

theorem isUniformInducing_toContinuousMap : IsUniformInducing fun α : FunSpace t₀ x₀ r L ↦ α.toContinuousMap :=
  ⟨rfl⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru