restrict_apply — Mathlib

English

If j ⊆ i and both i, j are measurable, restricting to i does not change v on j: v.restrict i j = v(j).

Русский

Если j ⊆ i и оба множества измеримы, ограничение до i не меняет меру на j: v.restrict i j = v(j).

LaTeX

$$$$ \\text{If } j \\subseteq i, \\; \\mathrm{MeasurableSet}(i), \\mathrm{MeasurableSet}(j) \\Rightarrow v.restrict i j = v(j). $$$$

Lean4

theorem restrict_apply {i : Set α} (hi : MeasurableSet i) {j : Set α} (hj : MeasurableSet j) :
    v.restrict i j = v (j ∩ i) := by
  rw [restrict, dif_pos hi]
  exact if_pos hj

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