uniformContinuousConstSMul — Mathlib

English

If a uniform continuous smul structure exists on X, then it lifts to the opposite type Xᵐᵒᵖ with uniform continuity preserved.

Русский

Если на X существует равномерно непрерывное действие, то это переносится на X^{op} с сохранением равномерной непрерывности.

LaTeX

$$$UniformContinuousConstSMul\; M\; X^{\mathrm{op}}$$$

Lean4

@[to_additive]
instance uniformContinuousConstSMul [UniformContinuousConstSMul M X] : UniformContinuousConstSMul M Xᵐᵒᵖ :=
  ⟨fun c => MulOpposite.uniformContinuous_op.comp <| MulOpposite.uniformContinuous_unop.const_smul c⟩

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