instCompleteSpace — Mathlib

English

IsComplete for FunSpace given a complete E.

Русский

IsComplete для FunSpace при полном E.

LaTeX

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

Lean4

/-- We show that `FunSpace` is complete in order to apply the contraction mapping theorem. -/
instance [CompleteSpace E] : CompleteSpace (FunSpace t₀ x₀ r L) :=
  by
  rw [completeSpace_iff_isComplete_range isUniformInducing_toContinuousMap]
  apply IsClosed.isComplete
  rw [range_toContinuousMap, setOf_and]
  apply isClosed_setOf_lipschitzWith L |>.preimage continuous_coeFun |>.inter
  simp_rw [mem_closedBall_iff_norm]
  exact isClosed_le (by fun_prop) continuous_const

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