ext_iff'

Mathlib.MeasureTheory.VectorMeasure.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.VectorMeasure.ext_iff'

English

Two vector measures are equal if and only if they agree on every subset.

Русский

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

LaTeX

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

Lean4

theorem ext_iff' (v w : VectorMeasure α M) : v = w ↔ ∀ i : Set α, v i = w i := by
  rw [← coe_injective.eq_iff, funext_iff]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru