lineMap_strict_mono_endpoints — Mathlib

English

If a < a' and r < 1, then lineMap(a,b,r) < lineMap(a',b,r).

Русский

Если a < a' и r < 1, то lineMap(a,b,r) < lineMap(a',b,r).

LaTeX

$$$ a < a' \land r < 1 \Rightarrow lineMap(a,b,r) < lineMap(a',b,r) $$$

Lean4

theorem lineMap_strict_mono_endpoints (ha : a < a') (hb : b < b') (h₀ : 0 ≤ r) (h₁ : r ≤ 1) :
    lineMap a b r < lineMap a' b' r := by
  rcases h₀.eq_or_lt with (rfl | h₀); · simpa
  exact (lineMap_mono_left ha.le h₁).trans_lt (lineMap_strict_mono_right hb h₀)

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