Theorems · Theorem · geometry

map_le_lineMap_iff_slope_le_slope_left

∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [inst_5 : Module k E] [IsStrictOrderedModule k E]
  [PosSMulReflectLE k E] {f : k → E} {a b r : k},
  0 < r * (b - a) →
    (f ((AffineMap.lineMap a b) r) ≤ (AffineMap.lineMap (f a) (f b)) r ↔
      slope f a ((AffineMap.lineMap a b) r) ≤ slope f a b)

Given c = lineMap a b r, a < c, the point (c, f c) is non-strictly below the segment [(a, f a), (b, f b)] if and only if slope f a c ≤ slope f a b.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Ordered

Cited by

3 results in Mathlib

Foundations

Depth 47 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderAddCommGroupPartialOrderIsOrderedAddMonoidModuleIsStrictOrderedModulePosSMulReflectLE