instContinuousConstSMulULift — Mathlib

English

If α is a topological space with a continuous action of M, then the induced action of ULift M on α is continuous. Equivalently, for every a ∈ α, the map γ ↦ (ULift.down γ) • a is continuous on ULift M.

Русский

Пусть α — топологическое пространство с непрерывным действием M. Тогда на α действует непрерывно индукированное действие ULift M: для каждого a ∈ α отображение γ ↦ (ULift.down γ) • a непрерывно по γ в ULift M.

LaTeX

$$$\forall a \in \alpha,\\; \text{Continuous}(\lambda \gamma: \mathrm{ULift} M, (\mathrm{ULift.down}\ \gamma) \cdot a).$$$

Lean4

@[to_additive]
instance : ContinuousConstSMul (ULift M) α :=
  ⟨fun γ ↦ continuous_const_smul (ULift.down γ)⟩

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