mul — Mathlib

English

If f and g are continuous on a set s, then their product is continuous on s.

Русский

Если f и g непрерывны на множестве s, то их произведение непрерывно на s.

LaTeX

$$$\\text{ContinuousOn } f s \\Rightarrow \\text{ContinuousOn } g s \\Rightarrow \\text{ContinuousOn } (\\lambda t. f t \\cdot g t) s$$$

Lean4

@[to_additive (attr := fun_prop)]
theorem mul (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun x => f x * g x) s := fun x hx ↦
  (hf x hx).mul (hg x hx)

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