isProbabilityMeasure — Mathlib

English

If for two finite index sets I,J and hJI: J ⊆ I, P I S = P J T whenever cylinder I S = cylinder J T.

Русский

Если для двух множеств индексов I,J и hJI: J ⊆ I, P I S = P J T тогда, когда cylinder I S = cylinder J T.

LaTeX

$$$\forall (I,J): Finset ι, (hJI : J \subseteq I)\to\forall {S:Set(Π i: I, α i)} {T:Set(Π i: J, α i)}\MeasurableSet S\ to\ MeasurableSet T\to\ cylinder I S = cylinder J T\Rightarrow P I S = P J T.$$$

Lean4

theorem isProbabilityMeasure [∀ i, IsProbabilityMeasure (P i)] (hμ : IsProjectiveLimit μ P) : IsProbabilityMeasure μ :=
  by
  constructor
  rw [hμ.measure_univ_eq (∅ : Finset ι)]
  exact measure_univ

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