ext_iff — Mathlib

English

Equality of vector measures is determined by values on measurable sets.

Русский

Равенство векторных мер определяется их значениями на измеримых множествах.

LaTeX

$$v = w ↔ ∀ i : Set α, MeasurableSet i → v(i) = w(i)$$

Lean4

theorem ext_iff (v w : VectorMeasure α M) : v = w ↔ ∀ i : Set α, MeasurableSet i → v i = w i :=
  by
  constructor
  · rintro rfl _ _
    rfl
  · rw [ext_iff']
    intro h i
    by_cases hi : MeasurableSet i
    · exact h i hi
    · simp_rw [not_measurable _ hi]

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