ext — Mathlib

English

If μ = generateFrom C, C is a Pi-system, μ has finite spanning sets in C, and μ and ν agree on all sets in C, then μ = ν.

Русский

Если μ = generateFrom(C), C — Pi‑система, μ имеет конечные генерирующие множества в C, и μ и ν совпадают на всех множествах из C, то μ = ν.

LaTeX

$$$hA : μ = generateFrom C \rightarrow hC : IsPiSystem C \rightarrow h : μ.FiniteSpanningSetsIn C \rightarrow (∀ s ∈ C, μ s = ν s) \rightarrow μ = ν$$$

Lean4

/-- An extensionality for measures. It is `ext_of_generateFrom_of_iUnion` formulated in terms of
`FiniteSpanningSetsIn`. -/
protected theorem ext {ν : Measure α} {C : Set (Set α)} (hA : ‹_› = generateFrom C) (hC : IsPiSystem C)
    (h : μ.FiniteSpanningSetsIn C) (h_eq : ∀ s ∈ C, μ s = ν s) : μ = ν :=
  ext_of_generateFrom_of_iUnion C _ hA hC h.spanning h.set_mem (fun i => (h.finite i).ne) h_eq

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