continuous_const_smul_iff — Mathlib

English

Let α be a topological space with a G-action by continuous scalar multiplication. For any function f: β → α and any fixed element c ∈ G, the map x ↦ c · f(x) is continuous if and only if f is continuous.

Русский

Пусть α — топологическое множество, на которое действует группа G через непрерывное скалярное умножение. Для любой функции f: β → α и фиксированного элемента c ∈ G отображение x ↦ c · f(x) непрерывно тогда и только тогда, когда f непрерывна.

LaTeX

$$$\operatorname{Continuous}(\lambda x\, . c \cdot f(x)) \iff \operatorname{Continuous}(f)$$$

Lean4

@[to_additive]
theorem continuous_const_smul_iff (c : G) : (Continuous fun x => c • f x) ↔ Continuous f := by
  simp only [continuous_iff_continuousAt, continuousAt_const_smul_iff]

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