English
If f and g are globally continuous, and for all x either f(x) ≠ 0 or g(x) ≠ ∞ and either g(x) ≠ 0 or f(x) ≠ ∞, then x ↦ f(x) · g(x) is continuous.
Русский
Если функции f и g непрерывны повсеместно, и для каждого x выполнены условия f(x) ≠ 0 или g(x) ≠ ∞, а также g(x) ≠ 0 или f(x) ≠ ∞, то x ↦ f(x) · g(x) непрерывна.
LaTeX
$$$\\\\text{Continuous } f \\\\land \\\\text{Continuous } g \\\\Rightarrow \\\\forall x, (f x ≠ 0 ∨ g x ≠ ∞) \\\\land (g x ≠ 0 ∨ f x ≠ ∞) \\\\Rightarrow \\\\text{Continuous } (x \\mapsto f x * g x).$$$
Lean4
theorem _root_.Continuous.ennreal_mul [TopologicalSpace α] {f g : α → ℝ≥0∞} (hf : Continuous f) (hg : Continuous g)
(h₁ : ∀ x, f x ≠ 0 ∨ g x ≠ ∞) (h₂ : ∀ x, g x ≠ 0 ∨ f x ≠ ∞) : Continuous fun x => f x * g x :=
continuous_iff_continuousAt.2 fun x => ENNReal.Tendsto.mul hf.continuousAt (h₁ x) hg.continuousAt (h₂ x)
