Theorems · Theorem · convex and discrete geometry

PointedCone.basis_coord_mem_dual

∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} (b : Module.Basis ι R M) (C : PointedCone R M),
  ↑C ⊆ ↑(PointedCone.hull R (Set.range ⇑b)) → ∀ (i : ι), b.coord i ∈ PointedCone.dual (Module.Dual.eval R M) ↑C

If a pointed cone C is contained in the conic hull of a basis b, then the coordinate functionals of b lie in the dual cone of C.

Defined in

Mathlib.Analysis.Convex.Cone.TensorProduct

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingPartialOrderIsOrderedRingAddCommGroupModule