IsProjectiveMeasureFamily — Mathlib

English

If the product space Π i, α_i is empty, then any projective measure P I is the zero measure for all finite I.

Русский

Если пространствa Π_i α_i пусто, то для всех конечных I мера P I равна нулевой.

LaTeX

$$$\text{If } (\prod_i \alpha_i) = \emptyset,\ \ P I = 0 \text{ for all } I.$$$

Lean4

/-- A family of measures indexed by finite sets of `ι` is projective if, for finite sets `J ⊆ I`,
the projection from `∀ i : I, α i` to `∀ i : J, α i` maps `P I` to `P J`. -/
def IsProjectiveMeasureFamily (P : ∀ J : Finset ι, Measure (∀ j : J, α j)) : Prop :=
  ∀ (I J : Finset ι) (hJI : J ⊆ I), P J = (P I).map (Finset.restrict₂ hJI)

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