continuous_compProj

Mathlib.Analysis.ODE.PicardLindelof

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

English

The map t ↦ α.compProj t is continuous for α ∈ FunSpace.

Русский

Карта t ↦ α.compProj t непрерывна для α ∈ FunSpace.

LaTeX

$$Continuous α.compProj$$

Lean4

@[continuity, fun_prop]
theorem continuous_compProj (α : FunSpace t₀ x₀ r L) : Continuous α.compProj :=
  α.continuous.comp continuous_projIcc

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

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

Разделы

Аффилиация

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