instInhabited

Mathlib.Analysis.ODE.PicardLindelof

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

Lean4

/-- `FunSpace t₀ x₀ r L` contains the constant map at `x₀`. -/
instance : Inhabited (FunSpace t₀ x₀ r L) :=
  ⟨fun _ ↦ x₀, (LipschitzWith.const _).weaken (zero_le _), mem_closedBall_self r.2⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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