toMeasureOfLEZero_apply — Mathlib

English

Restricting the zero vector measure remains zero.

Русский

Ограничение нулевой меры остаётся нулём.

LaTeX

$$$ \\text{restrict}(0) = 0 $$$

Lean4

theorem toMeasureOfLEZero_apply (hi : s ≤[i] 0) (hi₁ : MeasurableSet i) (hj₁ : MeasurableSet j) :
    s.toMeasureOfLEZero i hi₁ hi j =
      ((↑) : ℝ≥0 → ℝ≥0∞)
        ⟨-s (i ∩ j),
          neg_apply s (i ∩ j) ▸
            nonneg_of_zero_le_restrict _
              (zero_le_restrict_subset _ hi₁ Set.inter_subset_left
                (@neg_zero (VectorMeasure α ℝ) _ ▸ neg_le_neg _ _ hi₁ hi))⟩ :=
  by
  erw [toMeasureOfZeroLE_apply]
  · simp
  · assumption

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