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.

TODO

Is there a way to generalise IsClosed.upperClosure_pi/IsClosed.lowerClosure_pi so that they also apply to ℝ, ℝ × ℝ, EuclideanSpace ι ℝ? _pi has been appended to their names to disambiguate from the other possible lemmas, but we will want there to be a single set of lemmas for all situations.

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

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

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

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

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

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

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

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

theorem upperClosure_interior_subset' {α : Type u_1} [NormedOrderedGroup α] (s : Set α) : ↑(upperClosure (interior s)) ⊆ interior ↑(upperClosure s)

theorem upperClosure_interior_subset {α : Type u_1} [NormedOrderedAddGroup α] (s : Set α) : ↑(upperClosure (interior s)) ⊆ interior ↑(upperClosure s)

theorem lowerClosure_interior_subset' {α : Type u_1} [NormedOrderedGroup α] (s : Set α) : ↑(lowerClosure (interior s)) ⊆ interior ↑(lowerClosure s)

theorem lowerClosure_interior_subset {α : Type u_1} [NormedOrderedAddGroup α] (s : Set α) : ↑(lowerClosure (interior s)) ⊆ interior ↑(lowerClosure 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 dist_inf_sup_pi {ι : Type u_2} [Fintype ι] (x : ι → ℝ) (y : ι → ℝ) : dist (x ⊓ y) (x ⊔ y) = dist x y

theorem dist_mono_left_pi {ι : Type u_2} [Fintype ι] {y : ι → ℝ} : MonotoneOn (fun (x : ι → ℝ) => dist x y) (Set.Ici y)

theorem dist_mono_right_pi {ι : Type u_2} [Fintype ι] {x : ι → ℝ} : MonotoneOn (dist x) (Set.Ici x)

theorem dist_anti_left_pi {ι : Type u_2} [Fintype ι] {y : ι → ℝ} : AntitoneOn (fun (x : ι → ℝ) => dist x y) (Set.Iic y)

theorem dist_anti_right_pi {ι : Type u_2} [Fintype ι] {x : ι → ℝ} : AntitoneOn (dist x) (Set.Iic x)

theorem dist_le_dist_of_le_pi {ι : Type u_2} [Fintype ι] {a₁ : ι → ℝ} {a₂ : ι → ℝ} {b₁ : ι → ℝ} {b₂ : ι → ℝ} (ha : a₂ ≤ a₁) (h₁ : a₁ ≤ b₁) (hb : b₁ ≤ b₂) : dist a₁ b₁ ≤ dist a₂ b₂

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

Note

The closure and frontier of an antichain might not be antichains. Take for example the union of the open segments from (0, 2) to (1, 1) and from (2, 1) to (3, 0). (1, 1) and (2, 1) are comparable and both in the closure/frontier.

theorem IsClosed.upperClosure_pi {ι : Type u_2} [Finite ι] {s : Set (ι → ℝ)} (hs : IsClosed s) (hs' : BddBelow s) : IsClosed ↑(upperClosure s)

theorem IsClosed.lowerClosure_pi {ι : Type u_2} [Finite ι] {s : Set (ι → ℝ)} (hs : IsClosed s) (hs' : BddAbove s) : IsClosed ↑(lowerClosure s)

theorem IsClopen.upperClosure_pi {ι : Type u_2} [Finite ι] {s : Set (ι → ℝ)} (hs : IsClopen s) (hs' : BddBelow s) : IsClopen ↑(upperClosure s)

theorem IsClopen.lowerClosure_pi {ι : Type u_2} [Finite ι] {s : Set (ι → ℝ)} (hs : IsClopen s) (hs' : BddAbove s) : IsClopen ↑(lowerClosure s)

theorem closure_upperClosure_comm_pi {ι : Type u_2} [Finite ι] {s : Set (ι → ℝ)} (hs : BddBelow s) : closure ↑(upperClosure s) = ↑(upperClosure (closure s))

theorem closure_lowerClosure_comm_pi {ι : Type u_2} [Finite ι] {s : Set (ι → ℝ)} (hs : BddAbove s) : closure ↑(lowerClosure s) = ↑(lowerClosure (closure s))