Interiors of convex sets

A convex set symmetric about the origin has 0 in its interior as soon as its interior is nonempty. This lets volume arguments obtain the neighbourhood of the origin needed to use the gauge of a symmetric convex set.

The interior of a sum of two convex sets with nonempty interiors is the sum of their interiors. In particular, this describes the interior of the sum of two interval supports.

A closed segment segment 𝕜 x y is compact, being the continuous image of Icc 0 1.

theorem Convex.interior_add {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {s t : Set E} (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) (hsne : (interior s).Nonempty) (htne : (interior t).Nonempty) : interior (s + t) = interior s + interior t

The interior of a sum of convex sets with nonempty interiors is the sum of their interiors.

theorem Convex.zero_mem_interior_of_symmetric {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (hsymm : ∀ x ∈ s, -x ∈ s) (hi : (interior s).Nonempty) : 0 ∈ interior s

A convex set symmetric about the origin with nonempty interior has the origin in its interior.

theorem TauCeti.isCompact_segment (𝕜 : Type u_1) {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddRightMono 𝕜] [TopologicalSpace 𝕜] [CompactIccSpace 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] (x y : E) : IsCompact (segment 𝕜 x y)

A closed segment is compact: it is the continuous image of Icc 0 1.