Elementary faces of pointed cones #
Mathlib's ConvexCone.Salient records that a convex cone contains no line. This file records the
consequence of salience for the face lattice of a pointed cone: the zero cone is a face. It also
records that a face of a cone cuts out a face of every smaller cone.
Main declarations #
ConvexCone.Salient.bot_isFaceOf: the zero cone is a face of a salient pointed cone.PointedCone.IsFaceOf.inf_of_le: a face of a cone meets a smaller cone in a face of the smaller cone.
theorem
PointedCone.IsFaceOf.inf_of_le
{R : Type u_1}
{V : Type u_2}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
[AddCommGroup V]
[Module R V]
{C F τ : PointedCone R V}
(hF : F.IsFaceOf τ)
(hC : C ≤ τ)
:
(C ⊓ F).IsFaceOf C
A face F of a cone τ meets a cone C ≤ τ in a face of C.
theorem
ConvexCone.Salient.bot_isFaceOf
{R : Type u_1}
{V : Type u_2}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
[AddCommGroup V]
[Module R V]
[NoZeroSMulDivisors R V]
{C : PointedCone R V}
(hC : (↑C).Salient)
:
The zero cone is a face of a salient pointed cone.