measurableMul₂ — Mathlib

English

The product of two Borel spaces is a Borel space under SecondCountableTopology.

Русский

Произведение двух борелевских пространств является борелевским пространством при условии SecondCountable.

LaTeX

$$$\\{\\text{Prod.borelSpace}\\}$$$

Lean4

@[to_additive]
instance (priority := 100) measurableMul₂ [SecondCountableTopology γ] [Mul γ] [ContinuousMul γ] : MeasurableMul₂ γ :=
  ⟨continuous_mul.measurable⟩

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