coe_tsub — Mathlib

English

The coercion map to functions respects truncated subtraction: the function underlying f - g equals the pointwise subtraction f - g.

Русский

Промежуточное отображение в функции сохраняет усечённое вычитание: функция, соответствующая f − g, равна по точкам f(i) − g(i).

LaTeX

$$$ \forall f,g:\Pi₀ i, α_i,\forall i:\ (f - g)(i) = f(i) - g(i). $$$$

Lean4

@[simp, norm_cast]
theorem coe_tsub (f g : Π₀ i, α i) : ⇑(f - g) = f - g := by
  ext i
  exact tsub_apply f g i

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