Theorems · Definition · convex and discrete geometry

openSegment

(𝕜 : Type u_1) → {E : Type u_2} → [Semiring 𝕜] → [PartialOrder 𝕜] → [AddCommMonoid E] → [SMul 𝕜 E] → E → E → Set E

Open segment in a vector space. Note that openSegment 𝕜 x x = {x} instead of being ∅ when the base semiring has some element between 0 and 1.

Defined in

Mathlib.Analysis.Convex.Segment

Cited by

102 results in Mathlib

Foundations

Depth 12 from the axioms, rests on 119 definitions · uses no axioms

Assumes

SemiringPartialOrderAddCommMonoidSMul