ext — Mathlib

English

Two measures are equal if they agree on all measurable sets: ext.

Русский

Две меры равны, если они совпадают на всех измеримых множествах: экстенсионность меры.

LaTeX

$$$\mu_1 = \mu_2 \iff \forall s\ (MeasurableSet\ s)\ ,\mu_1(s)=\mu_2(s)$$$

Lean4

@[ext]
theorem ext (h : ∀ s, MeasurableSet s → μ₁ s = μ₂ s) : μ₁ = μ₂ :=
  toOuterMeasure_injective <| by rw [← trimmed, OuterMeasure.trim_congr (h _), trimmed]

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