Theorems · Theorem · geometry

map_le_lineMap_iff_slope_le_slope_right

∀ {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 < (1 - r) * (b - a) →
    (f ((AffineMap.lineMap a b) r) ≤ (AffineMap.lineMap (f a) (f b)) r ↔
      slope f a b ≤ slope f ((AffineMap.lineMap a b) r) b)

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

Defined in

Mathlib.LinearAlgebra.AffineSpace.Ordered

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderAddCommGroupPartialOrderIsOrderedAddMonoidModuleIsStrictOrderedModulePosSMulReflectLE