continuous_algebraMap_iff_smul — Mathlib

English

Continuity of the algebra map is equivalent to continuity of the map (r,a) ↦ r • a when [ContinuousMul A] holds.

Русский

Непрерывность алгебраического отображения эквивалентна непрерывности отображения (r,a) ↦ r • a при условии [ContinuousMul A].

LaTeX

$$$\text{Continuous algebra map} \iff \text{Continuous}(\lambda p : R \times A, p_1 \cdot p_2)$$$

Lean4

theorem continuous_algebraMap_iff_smul [ContinuousMul A] :
    Continuous (algebraMap R A) ↔ Continuous fun p : R × A => p.1 • p.2 :=
  by
  refine
    ⟨fun h => ?_, fun h =>
      have : ContinuousSMul R A := ⟨h⟩;
      continuous_algebraMap _ _⟩
  simp only [Algebra.smul_def]
  exact (h.comp continuous_fst).mul continuous_snd

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