unique — Mathlib

English

μ is the projective limit of P if for every finite I, μ maps to P I under the projection.

Русский

μ есть проективный предел P, если для каждого конечного I отображение проекции даёт P I.

LaTeX

$$$\forall I: Finset ι,\ (μ.map I.restrict) = P I.$$$

Lean4

/-- The projective limit of a family of finite measures is unique. -/
theorem unique [∀ i, IsFiniteMeasure (P i)] (hμ : IsProjectiveLimit μ P) (hν : IsProjectiveLimit ν P) : μ = ν :=
  by
  haveI : IsFiniteMeasure μ := hμ.isFiniteMeasure
  refine
    ext_of_generate_finite (measurableCylinders α) generateFrom_measurableCylinders.symm isPiSystem_measurableCylinders
      (fun s hs ↦ ?_) (hμ.measure_univ_unique hν)
  obtain ⟨I, S, hS, rfl⟩ := (mem_measurableCylinders _).mp hs
  rw [hμ.measure_cylinder _ hS, hν.measure_cylinder _ hS]

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