mul — Mathlib

English

If f and g are continuous at x, then their product is continuous at x.

Русский

Если f и g непрерывны в точке x, то их произведение непрерывно в x.

LaTeX

$$$\\text{ContinuousAt } f x \\land \\text{ContinuousAt } g x \\Rightarrow \\text{ContinuousAt } (\\lambda t. f t \\cdot g t) x$$$

Lean4

@[to_additive (attr := fun_prop)]
theorem mul (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun x => f x * g x) x :=
  Filter.Tendsto.mul hf hg

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