weightedSMul_congr — Mathlib

English

If μ s = μ t, then weightedSMul μ s = weightedSMul μ t.

Русский

Если меры объема по множествам s и t равны, то взвешенная карты по s и по t совпадают.

LaTeX

$$$$weightedSMul\,\mu\, s = weightedSMul\,\mu\, t \quad\text{whenever } μ s = μ t.$$$$

Lean4

theorem weightedSMul_congr (s t : Set α) (hst : μ s = μ t) : (weightedSMul μ s : F →L[ℝ] F) = weightedSMul μ t := by
  ext1 x; simp_rw [weightedSMul_apply, measureReal_def]; congr 2

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