mathlib3 documentation

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} [normed_ordered_group α] {s : set α} (hs : is_upper_set s) (ε : ) :
@[protected]
theorem is_upper_set.thickening {α : Type u_1} [normed_ordered_add_group α] {s : set α} (hs : is_upper_set s) (ε : ) :
@[protected]
theorem is_lower_set.thickening' {α : Type u_1} [normed_ordered_group α] {s : set α} (hs : is_lower_set s) (ε : ) :
@[protected]
theorem is_lower_set.thickening {α : Type u_1} [normed_ordered_add_group α] {s : set α} (hs : is_lower_set s) (ε : ) :
@[protected]
theorem is_upper_set.cthickening {α : Type u_1} [normed_ordered_add_group α] {s : set α} (hs : is_upper_set s) (ε : ) :
@[protected]
theorem is_upper_set.cthickening' {α : Type u_1} [normed_ordered_group α] {s : set α} (hs : is_upper_set s) (ε : ) :
@[protected]
theorem is_lower_set.cthickening {α : Type u_1} [normed_ordered_add_group α] {s : set α} (hs : is_lower_set s) (ε : ) :
@[protected]
theorem is_lower_set.cthickening' {α : Type u_1} [normed_ordered_group α] {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 closure s) (h : (i : ι), x i < y i) :
theorem is_lower_set.mem_interior_of_forall_lt {ι : Type u_2} [finite ι] {s : set )} {x y : ι } (hs : is_lower_set s) (hx : x closure s) (h : (i : ι), y i < x i) :
theorem is_upper_set.exists_subset_ball {ι : Type u_2} [fintype ι] {s : set )} {x : ι } {δ : } (hs : is_upper_set s) (hx : x closure s) (hδ : 0 < δ) :
theorem is_lower_set.exists_subset_ball {ι : Type u_2} [fintype ι] {s : set )} {x : ι } {δ : } (hs : is_lower_set s) (hx : x closure s) (hδ : 0 < δ) :