le_iff

Mathlib.MeasureTheory.VectorMeasure.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.VectorMeasure.le_iff

English

The order relation on vector measures is characterized by pointwise comparison on all measurable sets.

Русский

Отношение порядка на векторных мерах задаётся покомпьютерно по всем измеримым множествам.

LaTeX

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

Lean4

theorem le_iff : v ≤ w ↔ ∀ i, MeasurableSet i → v i ≤ w i :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru