compProj — Mathlib

English

For any α in FunSpace and t ∈ ℝ, α.compProj t = α(projIcc tmin tmax (le_trans t0.2.1 t0.2.2) t).

Русский

Для любого α в FunSpace и любого t, α.compProj t = α( projIcc tmin tmax (le_trans t0.2.1 t0.2.2) t ).

LaTeX

$$$\\alpha.compProj\\, t = \\alpha(\\operatorname{projIcc}(t_{min},t_{max},\\,\\underbrace{(t_0.2.1)}_{t_0.1}, \\underbrace{(t_0.2.2)}_{t}}))$$$

Lean4

/-- Extend the domain of `α` from `Icc tmin tmax` to `ℝ` such that `α t = α tmin` for all `t ≤ tmin`
and `α t = α tmax` for all `t ≥ tmax`. -/
noncomputable def compProj (α : FunSpace t₀ x₀ r L) (t : ℝ) : E :=
  α <| projIcc tmin tmax (le_trans t₀.2.1 t₀.2.2) t

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