# mathlib3documentation

analysis.normed.order.upper_lower

# Upper/lower/order-connected sets in normed groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

@[protected]
theorem is_upper_set.thickening' {α : Type u_1} {s : set α} (hs : is_upper_set s) (ε : ) :
@[protected]
theorem is_upper_set.thickening {α : Type u_1} {s : set α} (hs : is_upper_set s) (ε : ) :
@[protected]
theorem is_lower_set.thickening' {α : Type u_1} {s : set α} (hs : is_lower_set s) (ε : ) :
@[protected]
theorem is_lower_set.thickening {α : Type u_1} {s : set α} (hs : is_lower_set s) (ε : ) :
@[protected]
theorem is_upper_set.cthickening {α : Type u_1} {s : set α} (hs : is_upper_set s) (ε : ) :
@[protected]
theorem is_upper_set.cthickening' {α : Type u_1} {s : set α} (hs : is_upper_set s) (ε : ) :
@[protected]
theorem is_lower_set.cthickening {α : Type u_1} {s : set α} (hs : is_lower_set s) (ε : ) :
@[protected]
theorem is_lower_set.cthickening' {α : Type u_1} {s : set α} (hs : is_lower_set s) (ε : ) :

### ℝⁿ#

theorem is_upper_set.mem_interior_of_forall_lt {ι : Type u_2} [finite ι] {s : set )} {x y : ι } (hs : is_upper_set s) (hx : x ) (h : (i : ι), x i < y i) :
y
theorem is_lower_set.mem_interior_of_forall_lt {ι : Type u_2} [finite ι] {s : set )} {x y : ι } (hs : is_lower_set s) (hx : x ) (h : (i : ι), y i < x i) :
y
theorem dist_inf_sup {ι : Type u_2} [fintype ι] (x y : ι ) :
has_dist.dist (x y) (x y) =
theorem dist_mono_left {ι : Type u_2} [fintype ι] {y : ι } :
monotone_on (λ (x : ι ), y) (set.Ici y)
theorem dist_mono_right {ι : Type u_2} [fintype ι] {x : ι } :
(set.Ici x)
theorem dist_anti_left {ι : Type u_2} [fintype ι] {y : ι } :
antitone_on (λ (x : ι ), y) (set.Iic y)
theorem dist_anti_right {ι : Type u_2} [fintype ι] {x : ι } :
(set.Iic x)
theorem dist_le_dist_of_le {ι : Type u_2} [fintype ι] {a₁ a₂ b₁ b₂ : ι } (ha : a₂ a₁) (h₁ : a₁ b₁) (hb : b₁ b₂) :
b₁ b₂
@[protected]
theorem metric.bounded.bdd_below {ι : Type u_2} [fintype ι] {s : set )} :
@[protected]
theorem metric.bounded.bdd_above {ι : Type u_2} [fintype ι] {s : set )} :
@[protected]
theorem bdd_below.bounded {ι : Type u_2} [fintype ι] {s : set )} :
@[protected]
theorem bdd_above.bounded {ι : Type u_2} [fintype ι] {s : set )} :
theorem bounded_iff_bdd_below_bdd_above {ι : Type u_2} [fintype ι] {s : set )} :
theorem bdd_below.bounded_inter {ι : Type u_2} [fintype ι] {s t : set )} (hs : bdd_below s) (ht : bdd_above t) :
theorem bdd_above.bounded_inter {ι : Type u_2} [fintype ι] {s t : set )} (hs : bdd_above s) (ht : bdd_below t) :
theorem is_upper_set.exists_subset_ball {ι : Type u_2} [fintype ι] {s : set )} {x : ι } {δ : } (hs : is_upper_set s) (hx : x ) (hδ : 0 < δ) :
(y : ι ), / 4) / 4)
theorem is_lower_set.exists_subset_ball {ι : Type u_2} [fintype ι] {s : set )} {x : ι } {δ : } (hs : is_lower_set s) (hx : x ) (hδ : 0 < δ) :
(y : ι ), / 4) / 4)
theorem is_antichain.interior_eq_empty {ι : Type u_2} [finite ι] {s : set )} [nonempty ι] (hs : 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.

@[protected]
theorem is_closed.upper_closure {ι : Type u_2} [finite ι] {s : set )} (hs : is_closed s) (hs' : bdd_below s) :
@[protected]
theorem is_closed.lower_closure {ι : Type u_2} [finite ι] {s : set )} (hs : is_closed s) (hs' : bdd_above s) :
@[protected]
theorem is_clopen.upper_closure {ι : Type u_2} [finite ι] {s : set )} (hs : is_clopen s) (hs' : bdd_below s) :
@[protected]
theorem is_clopen.lower_closure {ι : Type u_2} [finite ι] {s : set )} (hs : is_clopen s) (hs' : bdd_above s) :
theorem closure_upper_closure_comm {ι : Type u_2} [finite ι] {s : set )} (hs : bdd_below s) :
theorem closure_lower_closure_comm {ι : Type u_2} [finite ι] {s : set )} (hs : bdd_above s) :