toMeasureOfZeroLE' — Mathlib

English

For any r, if v ⟂ᵥ w then r • v ⟂ᵥ w.

Русский

Для любого r: если v ⟂ᵥ w, то r • v ⟂ᵥ w.

LaTeX

$$$ v \\perp_{\\mathcal{V}} w \\Rightarrow (r \\cdot v) \\perp_{\\mathcal{V}} w $$$

Lean4

/-- The underlying function for `SignedMeasure.toMeasureOfZeroLE`. -/
def toMeasureOfZeroLE' (s : SignedMeasure α) (i : Set α) (hi : 0 ≤[i] s) (j : Set α) (hj : MeasurableSet j) : ℝ≥0∞ :=
  ((↑) : ℝ≥0 → ℝ≥0∞) ⟨s.restrict i j, le_trans (by simp) (hi j hj)⟩

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