div_const — Mathlib

English

If f is continuous on a set, then x ↦ f(x)/y is continuous on that set for any y.

Русский

Если f непрерывна на множестве, то x ↦ f(x)/y непрерывно на этом множестве для любого y.

LaTeX

$$$\\forall y,\\; \\mathrm{ContinuousOn}(f, s) \\Rightarrow \\mathrm{ContinuousOn}(\\lambda x. f(x)/y, s)$$$

Lean4

theorem div_const (hf : ContinuousOn f s) (y : G₀) : ContinuousOn (fun x => f x / y) s := by
  simpa only [div_eq_mul_inv] using hf.mul continuousOn_const

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