English
If f and g are continuous on s and g(x) ≠ 0 for all x ∈ s, then f/g is continuous on s.
Русский
Если f и g непрерывны на s и ∀x ∈ s, g(x) ≠ 0, то f/g непрерывна на s.
LaTeX
$$ContinuousOn f s → ContinuousOn g s → (∀ x ∈ s, g x ≠ 0) → ContinuousOn (\\lambda x, f(x) / g(x)) s$$
Lean4
/-- `h x (f x / g x)` is continuous under certain conditions, even if the denominator is sometimes
`0`. See docstring of `ContinuousAt.comp_div_cases`. -/
theorem comp_div_cases {f g : α → G₀} (h : α → G₀ → β) (hf : Continuous f) (hg : Continuous g)
(hh : ∀ a, g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)) (h2h : ∀ a, g a = 0 → Tendsto ↿h (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))) :
Continuous fun x => h x (f x / g x) :=
continuous_iff_continuousAt.mpr fun a => hf.continuousAt.comp_div_cases _ hg.continuousAt (hh a) (h2h a)
