continuous_mul_const — Mathlib

English

For ENNReal, the map x ↦ x · a is continuous at every x provided a ≠ 0 or x ≠ ∞.

Русский

Для ENNReal отображение x ↦ x · a непрерывно в любой точке x, если a ≠ 0 или x ≠ ∞.

LaTeX

$$$\\\\forall a, x, (a \\\\neq 0 \\\\lor x \\\\neq ∞) \\\\Rightarrow \\\\text{ContinuousAt } (\\\\lambda t, t * a) \\\\ x.$$$

Lean4

@[fun_prop]
protected theorem continuous_mul_const {a : ℝ≥0∞} (ha : a ≠ ∞) : Continuous fun x => x * a :=
  continuous_iff_continuousAt.2 fun _ => ENNReal.continuousAt_mul_const (Or.inl ha)

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