Exhausting a convex open set from inside

A convex open subset Ω of a proper real normed space — a finite-dimensional one, say — is the increasing union of convex open subsets whose closures are compact subsets of Ω. Intersecting the homothetic copies c + t • (Ω - c) about a point c ∈ Ω, for 0 < t < 1, with expanding balls gives the subsets: convexity keeps their closures inside Ω, the balls make them bounded, and properness makes their closures compact. Properness cannot be dropped: in an infinite-dimensional normed space the unit ball is exhausted by no sequence of relatively compact open subsets.

Convexity of the pieces is the point of the construction. A general open set is exhausted by the relatively compact open sets {x | dist x Ωᶜ > 1 / n} ∩ ball 0 n, but those are not convex, and an estimate whose constant depends on convexity of the domain — a Poincaré-type inequality, say — cannot be transported along them.

Main declaration

• TauCeti.exists_seq_isOpen_convex_isCompact_closure_subset_iUnion_eq: the exhaustion.

theorem TauCeti.exists_seq_isOpen_convex_isCompact_closure_subset_iUnion_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E] {Ω : Set E} (hΩ : IsOpen Ω) (hconv : Convex ℝ Ω) : ∃ (U : ℕ → Set E), Monotone U ∧ (∀ (n : ℕ), IsOpen (U n)) ∧ (∀ (n : ℕ), Convex ℝ (U n)) ∧ (∀ (n : ℕ), IsCompact (closure (U n))) ∧ (∀ (n : ℕ), closure (U n) ⊆ Ω) ∧ ⋃ (n : ℕ), U n = Ω

A convex open set is exhausted from inside by convex open sets. In a proper real normed space, if Ω is open and convex, there is an increasing sequence of convex open sets U n whose closures are compact subsets of Ω and whose union is Ω.