Theorems · Theorem · convex and discrete geometry

PointedCone.minTensorProduct_eq_max_of_simplicial_generating_left

∀ {E : Type u_1} {F : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace F] [IsTopologicalAddGroup F] [T2Space F] [FiniteDimensional ℝ F]
  [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] (C₁ : PointedCone ℝ E) (C₂ : ProperCone ℝ F),
  C₁.IsSimplicial → Submodule.span ℝ ↑C₁ = ⊤ → C₁.minTensorProduct ↑C₂ = C₁.maxTensorProduct ↑C₂

If C₁ is a simplicial and generating cone and C₂ is a proper cone, then their minimal and maximal tensor products are equal.

Defined in

Mathlib.Analysis.Convex.Cone.TensorProduct

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommGroupModuleAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupT2SpaceFiniteDimensionalContinuousSMulLocallyConvexSpace