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
upper_closure_interior_subset
{α : Type u_1}
[normed_ordered_add_group α]
(s : set α) :
↑(upper_closure (interior s)) ⊆ interior ↑(upper_closure s)
theorem
upper_closure_interior_subset'
{α : Type u_1}
[normed_ordered_group α]
(s : set α) :
↑(upper_closure (interior s)) ⊆ interior ↑(upper_closure s)
theorem
lower_closure_interior_subset'
{α : Type u_1}
[normed_ordered_group α]
(s : set α) :
↑(upper_closure (interior s)) ⊆ interior ↑(upper_closure s)
theorem
lower_closure_interior_subset
{α : Type u_1}
[normed_ordered_add_group α]
(s : set α) :
↑(upper_closure (interior s)) ⊆ interior ↑(upper_closure s)
ℝⁿ #
theorem
dist_inf_sup
{ι : Type u_2}
[fintype ι]
(x y : ι → ℝ) :
has_dist.dist (x ⊓ y) (x ⊔ y) = has_dist.dist x y
theorem
dist_mono_left
{ι : Type u_2}
[fintype ι]
{y : ι → ℝ} :
monotone_on (λ (x : ι → ℝ), has_dist.dist x y) (set.Ici y)
theorem
dist_mono_right
{ι : Type u_2}
[fintype ι]
{x : ι → ℝ} :
monotone_on (has_dist.dist x) (set.Ici x)
theorem
dist_anti_left
{ι : Type u_2}
[fintype ι]
{y : ι → ℝ} :
antitone_on (λ (x : ι → ℝ), has_dist.dist x y) (set.Iic y)
theorem
dist_anti_right
{ι : Type u_2}
[fintype ι]
{x : ι → ℝ} :
antitone_on (has_dist.dist 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₂) :
has_dist.dist a₁ b₁ ≤ has_dist.dist a₂ b₂
@[protected]
theorem
metric.bounded.bdd_below
{ι : Type u_2}
[fintype ι]
{s : set (ι → ℝ)} :
metric.bounded s → bdd_below s
@[protected]
theorem
metric.bounded.bdd_above
{ι : Type u_2}
[fintype ι]
{s : set (ι → ℝ)} :
metric.bounded s → bdd_above 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
closure_upper_closure_comm
{ι : Type u_2}
[finite ι]
{s : set (ι → ℝ)}
(hs : bdd_below s) :
closure ↑(upper_closure s) = ↑(upper_closure (closure s))
theorem
closure_lower_closure_comm
{ι : Type u_2}
[finite ι]
{s : set (ι → ℝ)}
(hs : bdd_above s) :
closure ↑(lower_closure s) = ↑(lower_closure (closure s))