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} [NormedCommGroup α] [Preorder α] [IsOrderedMonoid α] {s : Set α} (hs : IsUpperSet s) (ε : ℝ) : IsUpperSet (Metric.thickening ε s)

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

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

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

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

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

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

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

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

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

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

theorem lowerClosure_interior_subset {α : Type u_1} [NormedAddCommGroup α] [Preorder α] [IsOrderedAddMonoid α] (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 {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [IsOrderedAddMonoid α] [HasSolidNorm α] (x y : α) : dist (x ⊓ y) (x ⊔ y) = dist x y

theorem dist_mono_left {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [IsOrderedAddMonoid α] [HasSolidNorm α] {y : α} : MonotoneOn (fun (x : α) => dist x y) (Set.Ici y)

theorem dist_mono_right {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [IsOrderedAddMonoid α] [HasSolidNorm α] {x : α} : MonotoneOn (dist x) (Set.Ici x)

theorem dist_anti_left {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [IsOrderedAddMonoid α] [HasSolidNorm α] {y : α} : AntitoneOn (fun (x : α) => dist x y) (Set.Iic y)

theorem dist_anti_right {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [IsOrderedAddMonoid α] [HasSolidNorm α] {x : α} : AntitoneOn (dist x) (Set.Iic x)

theorem dist_le_dist_of_le {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [IsOrderedAddMonoid α] [HasSolidNorm α] {a₁ a₂ b₁ b₂ : α} (ha : a₂ ≤ a₁) (h₁ : a₁ ≤ b₁) (hb : b₁ ≤ b₂) : dist a₁ b₁ ≤ dist a₂ b₂

@[deprecated dist_inf_sup (since := "2026-10-02")]

theorem dist_inf_sup_pi {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [IsOrderedAddMonoid α] [HasSolidNorm α] (x y : α) : dist (x ⊓ y) (x ⊔ y) = dist x y

Alias of dist_inf_sup.

@[deprecated dist_mono_left (since := "2026-10-02")]

theorem dist_mono_left_pi {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [IsOrderedAddMonoid α] [HasSolidNorm α] {y : α} : MonotoneOn (fun (x : α) => dist x y) (Set.Ici y)

Alias of dist_mono_left.

@[deprecated dist_mono_right (since := "2026-10-02")]

theorem dist_mono_right_pi {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [IsOrderedAddMonoid α] [HasSolidNorm α] {x : α} : MonotoneOn (dist x) (Set.Ici x)

Alias of dist_mono_right.

@[deprecated dist_anti_left (since := "2026-10-02")]

theorem dist_anti_left_pi {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [IsOrderedAddMonoid α] [HasSolidNorm α] {y : α} : AntitoneOn (fun (x : α) => dist x y) (Set.Iic y)

Alias of dist_anti_left.

@[deprecated dist_anti_right (since := "2026-10-02")]

theorem dist_anti_right_pi {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [IsOrderedAddMonoid α] [HasSolidNorm α] {x : α} : AntitoneOn (dist x) (Set.Iic x)

Alias of dist_anti_right.

@[deprecated dist_le_dist_of_le (since := "2026-10-02")]

theorem dist_le_dist_of_le_pi {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [IsOrderedAddMonoid α] [HasSolidNorm α] {a₁ a₂ b₁ b₂ : α} (ha : a₂ ≤ a₁) (h₁ : a₁ ≤ b₁) (hb : b₁ ≤ b₂) : dist a₁ b₁ ≤ dist a₂ b₂

Alias of dist_le_dist_of_le.

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))