div_const — Mathlib

English

If f is continuous, then the map x ↦ f x / y is continuous for any y; i.e., division by a constant is continuous.

Русский

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

LaTeX

$$$\\mathrm{Continuous}\\left( x \\mapsto \\dfrac{f(x)}{y} \\right)$$$

Lean4

@[continuity, fun_prop]
theorem div_const (hf : Continuous f) (y : G₀) : Continuous fun x => f x / y := by
  simpa only [div_eq_mul_inv] using hf.mul continuous_const

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