English
If f and g are continuous on a set s, and for every x ∈ s one has either f(x) ≠ 0 or g(x) ≠ ∞ and either g(x) ≠ 0 or f(x) ≠ ∞, then x ↦ f(x) · g(x) is continuous on s.
Русский
Если функции f и g непрерывны на множесте s, и для каждого x ∈ s выполняется либо f(x) ≠ 0, либо g(x) ≠ ∞, и либо g(x) ≠ 0, либо f(x) ≠ ∞, то x ↦ f(x) · g(x) непрерывна на s.
LaTeX
$$$\\\\forall f,g: \\\\alpha \\to ENNReal, \\\\text{ContinuousOn } f \, s \\\\land \\\\text{ContinuousOn } g \, s \\\\land \\\\forall x \\in s, (f x ≠ 0 ∨ g x ≠ ∞) \\\\land \\\\forall x \\in s, (g x ≠ 0 ∨ f x ≠ ∞) \\\\Rightarrow \\\\text{ContinuousOn } (x \\mapsto f x * g x) \, s.$$$
Lean4
theorem _root_.ContinuousOn.ennreal_mul [TopologicalSpace α] {f g : α → ℝ≥0∞} {s : Set α} (hf : ContinuousOn f s)
(hg : ContinuousOn g s) (h₁ : ∀ x ∈ s, f x ≠ 0 ∨ g x ≠ ∞) (h₂ : ∀ x ∈ s, g x ≠ 0 ∨ f x ≠ ∞) :
ContinuousOn (fun x => f x * g x) s := fun x hx => ENNReal.Tendsto.mul (hf x hx) (h₁ x hx) (hg x hx) (h₂ x hx)
