continuousSMul_induced — Mathlib

English

Given a scalar action of R on M1 and a target M2 with a topology t, the induced topology on M2 via a map f yields a continuous scalar action on M1 by R. In particular, the induced topology makes the action of R on M1 continuous.

Русский

Пусть имеется действие скаляров R на M1 и задано топологическое пространство M2; если на M2 задана топология, индуцированная отображением f, то действие R на M1 непрерывно.

LaTeX

$$$\text{ContinuousSMul}_R(M_1, t_{induced\,f})$.$$

Lean4

theorem continuousSMul_induced : @ContinuousSMul R M₁ _ u (t.induced f) :=
  let _ : TopologicalSpace M₁ := t.induced f
  IsInducing.continuousSMul ⟨rfl⟩ continuous_id (map_smul f _ _)

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