Theorems · Theorem · convex and discrete geometry

openSegment.lift

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [ZeroLEOneClass 𝕜] [inst_4 : Module 𝕜 E] (R : Type u_7) [inst_5 : Semiring R] [inst_6 : PartialOrder R]
  [inst_7 : Module R E] [inst_8 : Module R 𝕜] [IsScalarTower R 𝕜 E] [Nontrivial 𝕜] [SMulPosStrictMono R 𝕜] (x y : E),
  openSegment R x y ⊆ openSegment 𝕜 x y

Defined in

Mathlib.Analysis.Convex.Segment

Cited by

0 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms

Assumes

SemiringPartialOrderAddCommMonoidZeroLEOneClassModuleSemiringPartialOrderModuleModuleIsScalarTowerNontrivialSMulPosStrictMono