neg_le_neg — Mathlib

English

Negation reverses the order on restricted sets: if v ≤[i] w then −w ≤[i] −v.

Русский

Отрицание разворачивает порядок на ограничениях: если v ≤[i] w, то −w ≤[i] −v.

LaTeX

$$$ (-w) \\restriction i \\le (-v) \\restriction i $$$

Lean4

nonrec theorem neg_le_neg {i : Set α} (hi : MeasurableSet i) (h : v ≤[i] w) : -w ≤[i] -v :=
  by
  intro j hj₁
  rw [restrict_apply _ hi hj₁, restrict_apply _ hi hj₁, neg_apply, neg_apply]
  refine neg_le_neg ?_
  rw [← restrict_apply _ hi hj₁, ← restrict_apply _ hi hj₁]
  exact h j hj₁

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