pi_def — Mathlib

English

The product measure π μ coincides with the outer-measure-based construction on the product space, as formalized by a certain equivalence.

Русский

Произведение меры π μ совпадает с конструкцией на основе внешней меры на произведении пространств.

LaTeX

$$pi μ = (OuterMeasure.pi (λ i, μ_i.toOuterMeasure)).toMeasure$$

Lean4

theorem pi_def : eta_helper Eq✝ @pi.{} @(delta% @definition✝) :=
  by
  intros
  delta pi
  rw [show wrapped✝ = ⟨@definition✝.{}, rfl✝⟩ from Subtype.ext✝ wrapped✝.2.symm✝]
  rfl

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