compProj_mem_closedBall — Mathlib

English

Under the same bound, α.compProj t ∈ closedBall x0 a for all t.

Русский

При тех же условиях, α.compProj t принадлежит замкнутому шару вокруг x0 радиуса a для всех t.

LaTeX

$$∀ t, α.compProj t ∈ closedBall(x0,a)$$

Lean4

theorem compProj_mem_closedBall (α : FunSpace t₀ x₀ r L) (h : L * max (tmax - t₀) (t₀ - tmin) ≤ a - r) {t : ℝ} :
    α.compProj t ∈ closedBall x₀ a := by
  rw [compProj_apply]
  exact α.mem_closedBall h

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