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)
(ε : ℝ) :