instPartialOrder — Mathlib

English

Vector measures form a partial order: v ≤ w iff v i ≤ w i for all measurable sets i.

Русский

Векторные меры образуют частичный порядок: v ≤ w тогда и только тогда, когда для всех измеримых множеств i выполняется v(i) ≤ w(i).

LaTeX

$$$ v \\le w \\iff \\forall i,\\, MeasurableSet(i) \\to v(i) \\le w(i) $$$

Lean4

/-- Vector measures over a partially ordered monoid is partially ordered.

This definition is consistent with `Measure.instPartialOrder`. -/
instance instPartialOrder : PartialOrder (VectorMeasure α M)
    where
  le v w := ∀ i, MeasurableSet i → v i ≤ w i
  le_refl _ _ _ := le_rfl
  le_trans _ _ _ h₁ h₂ i hi := le_trans (h₁ i hi) (h₂ i hi)
  le_antisymm _ _ h₁ h₂ := ext fun i hi => le_antisymm (h₁ i hi) (h₂ i hi)

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