lineMap_anti — Mathlib

English

If p1 ≤ p0 in V1, then lineMap(p0,p1,·) is antitone with respect to the order on k.

Русский

Если p1 ≤ p0 в V1, то lineMap(p0,p1,·) антимонотонна по отношению к порядку на k.

LaTeX

$$Antitone(lineMap(p_0,p_1)) при p_1 ≤ p_0$$

Lean4

theorem lineMap_anti [LinearOrder k] [Preorder V1] [AddLeftMono V1] [SMulPosMono k V1] {p₀ p₁ : V1} (h : p₁ ≤ p₀) :
    Antitone (lineMap (k := k) p₀ p₁) := by
  intro x y hxy
  suffices y • (p₁ - p₀) ≤ x • (p₁ - p₀) by simpa [lineMap]
  rw [← neg_le_neg_iff, ← smul_neg, ← smul_neg]
  gcongr
  simpa

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