Theorems · Theorem · convex and discrete geometry

Convex.mem_Ico

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

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

Defined in

Mathlib.Analysis.Convex.Segment

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRing