ProperCone.dual_dual
theorem ProperCone.dual_dual :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : CompleteSpace E]
(K : ProperCone ℝ E), K.dual.dual = K
This theorem states that for any proper cone `K` in a complete inner product space over the real numbers, which is also a normed additive commutative group, the dual of the dual of `K` is `K` itself. In other words, applying the dual operation twice to a proper cone brings us back to the original proper cone.
More concisely: The dual of a proper cone in a complete inner product space over the real numbers is equal to the original cone.
|
ProperCone.isClosed
theorem ProperCone.isClosed :
∀ {𝕜 : Type u_1} [inst : OrderedSemiring 𝕜] {E : Type u_2} [inst_1 : AddCommMonoid E] [inst_2 : TopologicalSpace E]
[inst_3 : Module 𝕜 E] (K : ProperCone 𝕜 E), IsClosed ↑K
The theorem `ProperCone.isClosed` states that for any given proper cone `K` in a module `E` over an ordered semi-ring `𝕜`, with `E` being a topological space and an additive commutative monoid, the set underlying `K` is closed in the topology of `E`. In other words, for any such mathematical structure, the theorem asserts that the proper cone `K` is a closed set.
More concisely: A proper cone in an ordered semi-ring module endowed with the topology of a topological space and being an additive commutative monoid is a closed set.
|
ProperCone.toPointedCone_injective
theorem ProperCone.toPointedCone_injective :
∀ {𝕜 : Type u_1} [inst : OrderedSemiring 𝕜] {E : Type u_2} [inst_1 : AddCommMonoid E] [inst_2 : TopologicalSpace E]
[inst_3 : Module 𝕜 E], Function.Injective ProperCone.toPointedCone
The theorem `ProperCone.toPointedCone_injective` asserts that for any ordered semiring `𝕜` and any type `E` that is an additively commutative monoid, a topological space and a module over `𝕜`, the function `ProperCone.toPointedCone` is injective. This means that for these conditions, if two proper cones in the context are mapped to the same pointed cone via the function `ProperCone.toPointedCone`, then the two initial proper cones must have been the same.
More concisely: For any ordered semiring `𝕜`, additively commutative monoid, topological space, and `𝕜`-module `E`, the function `ProperCone.toPointedCone` maps distinct proper cones to distinct pointed cones.
|