compProj_apply — Mathlib

English

The equality α.compProj t = α (projIcc tmin tmax (le_trans t0.2.1 t0.2.2) t) holds by definition.

Русский

Неравенство/тождество выполняется по определению: α.compProj t = α( projIcc ... ).

LaTeX

$$$\\alpha.compProj\\, t = \\alpha(\\operatorname{projIcc}(t_{min},t_{max},\\,\\ldots,t\\,))$$$

Lean4

@[simp]
theorem compProj_apply {α : FunSpace t₀ x₀ r L} {t : ℝ} :
    α.compProj t = α (projIcc tmin tmax (le_trans t₀.2.1 t₀.2.2) t) :=
  rfl

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