restrict_eq_self — Mathlib

English

For measurable i, measurable j, the restriction satisfies (v.restrict i)(j) = v(j ∩ i).

Русский

При измеримых i и j выполняется (v.restrict i)(j) = v(j ∩ i).

LaTeX

$$$$ (v.restrict i)(j) = v(j \\cap i) \\quad\\text{для } \\mathrm{MeasurableSet}(j). $$$$

Lean4

theorem restrict_eq_self {i : Set α} (hi : MeasurableSet i) {j : Set α} (hj : MeasurableSet j) (hij : j ⊆ i) :
    v.restrict i j = v j := by rw [restrict_apply v hi hj, Set.inter_eq_left.2 hij]

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