measurableSMul₂ — Mathlib

English

If γ is a SecondCountableTopology, Mul γ, ContinuousMul γ, then MeasurableMul₂ γ holds.

Русский

Если γ имеет SecondCountableTopology, Mul γ и ContinuousMul γ, то MeasurableMul₂ γ выполняется.

LaTeX

$$$\\mathrm{MeasurableMul₂}(\\gamma)$$$

Lean4

instance (priority := 100) measurableSMul₂ {M α} [TopologicalSpace M] [MeasurableSpace M] [OpensMeasurableSpace M]
    [TopologicalSpace α] [SecondCountableTopologyEither M α] [MeasurableSpace α] [BorelSpace α] [SMul M α]
    [ContinuousSMul M α] : MeasurableSMul₂ M α :=
  ⟨continuous_smul.measurable⟩

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