theorem
Set.zero_mem_of_zero_mem_cone_of_convex
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{D : Set E}
(hD_convex : Convex ℝ D)
(h0_cone : 0 ∈ D.cone)
:
0 ∈ D
Helper for Proposition 6.17: if the origin belongs to the cone of a convex set, then it already belongs to the set.
theorem
Set.cone_interior_eq_univ_of_zero_mem_interior
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{C : Set E}
(hC_convex : Convex ℝ C)
(h0_int : 0 ∈ interior C)
:
(interior C).cone = univ
Helper for Proposition 6.17: an interior neighborhood of the origin generates the whole space through the cone of the interior.
theorem
Set.zero_mem_interior_of_cone_interior_eq_univ
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{C : Set E}
(hC_convex : Convex ℝ C)
(hC_int_nonempty : (interior C).Nonempty)
(hcone : (interior C).cone = univ)
:
0 ∈ interior C
Helper for Proposition 6.17: if the cone of the interior is all of the ambient space, then the origin is an interior point.
theorem
Set.cone_interior_eq_univ_of_closure_cone_eq_univ
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{C : Set E}
(hC_convex : Convex ℝ C)
(hC_int_nonempty : (interior C).Nonempty)
(hclosure : closure C.cone = univ)
:
(interior C).cone = univ
Helper for Proposition 6.17: a dense cone over a convex set with nonempty interior already forces the cone of the interior to be the whole space.
theorem
Set.zero_mem_interior_tfae_cone_interior_cone_closure_eq_univ
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{C : Set E}
(hC_convex : Convex ℝ C)
(hC_int_nonempty : (interior C).Nonempty)
:
Proposition 6.17: for a convex subset C of a real normed space with nonempty interior, the
following are equivalent: (i) 0 ∈ interior C; (ii) cone (interior C) = univ; (iii)
cone C = univ; and (iv) closure (cone C) = univ.