coe_sub — Mathlib

English

The pointwise subtraction of two bounded continuous functions is again a bounded continuous function.

Русский

Поточечная разность двух ограниченных непрерывных функций вновь является ограниченной непрерывной функцией.

LaTeX

$$$f,g: \alpha \to^{\mathrm{b}} \mathbb{R} \implies (f-g) \in \alpha \to^{\mathrm{b}} \mathbb{R}$ with $(f-g)(x) = f(x)-g(x)$$$

Lean4

@[simp]
theorem coe_sub : ⇑(f - g) = f - g :=
  rfl

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