coe_injective — Mathlib

English

If two vector measures v and w assign the same value to every subset of α, then v = w.

Русский

Если две векторные меры v и w сопоставляют одно и то же значение каждому подмножеству α, тогда v = w.

LaTeX

$$($\\forall S: Set\\,\\alpha, v(S) = w(S)\\) implies $v = w$.$$

Lean4

theorem coe_injective : @Function.Injective (VectorMeasure α M) (Set α → M) (⇑) := fun v w h =>
  by
  cases v
  cases w
  congr

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