instNeg — Mathlib

English

The pointwise negation of a bounded continuous function is again bounded and continuous; i.e., -f ∈ α →ᵇ β and ∥-f∥ ≤ ∥f∥.

Русский

Точечно-негативная функция является ограниченной непрерывной: -f ∈ α →ᵇ β и ∥-f∥ ≤ ∥f∥.

LaTeX

$$$(-f) \in \alpha \to^b \beta$ and $\| -f \| ≤ \| f \|$.$$

Lean4

/-- The pointwise opposite of a bounded continuous function is again bounded continuous. -/
instance : Neg (α →ᵇ β) :=
  ⟨fun f => ofNormedAddCommGroup (-f) f.continuous.neg ‖f‖ fun x => norm_neg ((⇑f) x) ▸ f.norm_coe_le_norm x⟩

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