lineMap_mono — Mathlib

English

If p0 ≤ p1 in V1, then the function c ↦ lineMap(p0,p1,c) is monotone with respect to the order on k.

Русский

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

LaTeX

$$Monotone(lineMap(p_0,p_1)) \n при условии p_0 ≤ p_1 и подходящих структурных предположений на k и V1$$

Lean4

theorem lineMap_mono [LinearOrder k] [Preorder V1] [AddRightMono V1] [SMulPosMono k V1] {p₀ p₁ : V1} (h : p₀ ≤ p₁) :
    Monotone (lineMap (k := k) p₀ p₁) := by
  intro x y hxy
  suffices x • (p₁ - p₀) ≤ y • (p₁ - p₀) by simpa [lineMap]
  gcongr
  simpa

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