mul — Mathlib

English

If f and g are continuous within a set s at x, their product is continuous within s at x.

Русский

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

LaTeX

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

Lean4

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

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