neg_le_neg_iff

Mathlib.MeasureTheory.VectorMeasure.Basic

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

← MathLib Explorer

English

For measurable i, −w ≤[i] −v iff v ≤[i] w.

Русский

Для измеримого i: −w ≤[i] −v ⇔ v ≤[i] w.

LaTeX

$$$ -w \\restriction i \\le -v \\restriction i \\iff v \\restriction i \\le w \\restriction i $$$

Lean4

theorem neg_le_neg_iff {i : Set α} (hi : MeasurableSet i) : -w ≤[i] -v ↔ v ≤[i] w :=
  ⟨fun h => neg_neg v ▸ neg_neg w ▸ neg_le_neg _ _ hi h, fun h => neg_le_neg _ _ hi h⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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