IsProjectiveLimit — Mathlib

English

The projective limit μ of a family P is a measure on Π i, α i such that, for every finite J, its projection equals P J.

Русский

Проективный предел μ семейства P — мера на произведение, чья проекция на конечное множество J равна P J.

LaTeX

$$$\forall I,\ (\mu.map I.restrict) = P I.$$$

Lean4

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

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