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