Upper/lower/order-connected sets in normed groups

The topological closure and interior of an upper/lower/order-connected set is an upper/lower/order-connected set (with the notable exception of the closure of an order-connected set).

We also prove lemmas specific to ℝⁿ. Those are helpful to prove that order-connected sets in ℝⁿ are measurable.

theorem IsUpperSet.thickening {α : Type u_1} [NormedOrderedAddGroup α] {s : Set α} (hs : IsUpperSet s) (ε : ℝ) : IsUpperSet (Metric.thickening ε s)

theorem IsUpperSet.thickening' {α : Type u_1} [NormedOrderedGroup α] {s : Set α} (hs : IsUpperSet s) (ε : ℝ) : IsUpperSet (Metric.thickening ε s)

theorem IsLowerSet.thickening {α : Type u_1} [NormedOrderedAddGroup α] {s : Set α} (hs : IsLowerSet s) (ε : ℝ) : IsLowerSet (Metric.thickening ε s)

theorem IsLowerSet.thickening' {α : Type u_1} [NormedOrderedGroup α] {s : Set α} (hs : IsLowerSet s) (ε : ℝ) : IsLowerSet (Metric.thickening ε s)

theorem IsUpperSet.cthickening {α : Type u_1} [NormedOrderedAddGroup α] {s : Set α} (hs : IsUpperSet s) (ε : ℝ) : IsUpperSet (Metric.cthickening ε s)

theorem IsUpperSet.cthickening' {α : Type u_1} [NormedOrderedGroup α] {s : Set α} (hs : IsUpperSet s) (ε : ℝ) : IsUpperSet (Metric.cthickening ε s)

theorem IsLowerSet.cthickening {α : Type u_1} [NormedOrderedAddGroup α] {s : Set α} (hs : IsLowerSet s) (ε : ℝ) : IsLowerSet (Metric.cthickening ε s)

theorem IsLowerSet.cthickening' {α : Type u_1} [NormedOrderedGroup α] {s : Set α} (hs : IsLowerSet s) (ε : ℝ) : IsLowerSet (Metric.cthickening ε s)

ℝⁿ

theorem IsUpperSet.mem_interior_of_forall_lt {ι : Type u_2} [Finite ι] {s : Set (ι → ℝ)} {x : ι → ℝ} {y : ι → ℝ} (hs : IsUpperSet s) (hx : x ∈ closure s) (h : ∀ (i : ι), x i < y i) : y ∈ interior s

theorem IsLowerSet.mem_interior_of_forall_lt {ι : Type u_2} [Finite ι] {s : Set (ι → ℝ)} {x : ι → ℝ} {y : ι → ℝ} (hs : IsLowerSet s) (hx : x ∈ closure s) (h : ∀ (i : ι), y i < x i) : y ∈ interior s

theorem IsUpperSet.exists_subset_ball {ι : Type u_2} [Fintype ι] {s : Set (ι → ℝ)} {x : ι → ℝ} {δ : ℝ} (hs : IsUpperSet s) (hx : x ∈ closure s) (hδ : 0 < δ) : ∃ (y : ι → ℝ), Metric.closedBall y (δ / 4) ⊆ Metric.closedBall x δ ∧ Metric.closedBall y (δ / 4) ⊆ interior s

theorem IsLowerSet.exists_subset_ball {ι : Type u_2} [Fintype ι] {s : Set (ι → ℝ)} {x : ι → ℝ} {δ : ℝ} (hs : IsLowerSet s) (hx : x ∈ closure s) (hδ : 0 < δ) : ∃ (y : ι → ℝ), Metric.closedBall y (δ / 4) ⊆ Metric.closedBall x δ ∧ Metric.closedBall y (δ / 4) ⊆ interior s