instIsFiniteMeasure — Mathlib

English

For any sets s ⊆ α and t ⊆ β, μ × ν (s × t) equals μ(s) ν(t).

Русский

Для любых множеств s ⊆ α и t ⊆ β выполняется μ × ν (s × t) = μ(s) ν(t).

LaTeX

$$$\mu \mathrm{.prod} ν (s \timesˢ t) = μ(s) \cdot ν(t)$$$

Lean4

instance instIsFiniteMeasure {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : Measure α)
    (ν : Measure β) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : IsFiniteMeasure (μ.prod ν) :=
  by
  constructor
  rw [← univ_prod_univ, prod_prod]
  finiteness

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