Theorems · Theorem · convex and discrete geometry

Convex.mem_Icc

∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y z : 𝕜},
  x ≤ y → (z ∈ Set.Icc x y ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z)

A point is in an Icc iff it can be expressed as a convex combination of the endpoints.

Defined in

Mathlib.Analysis.Convex.Segment

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRing