Order-connected sets
We say that a set s : set α is ord_connected if for all x y ∈ s it includes the
interval [x, y]. If α is a densely_ordered conditionally_complete_linear_order with
the order_topology, then this condition is equivalent to is_preconnected s. If α = ℝ, then
this condition is also equivalent to convex s.
In this file we prove that intersection of a family of ord_connected sets is ord_connected and
that all standard intervals are ord_connected.
We say that a set s : set α is ord_connected if for all x y ∈ s it includes the
interval [x, y]. If α is a densely_ordered conditionally_complete_linear_order with
the order_topology, then this condition is equivalent to is_preconnected s. If α = ℝ, then
this condition is also equivalent to convex s.
theorem
set.ord_connected.inter
{α : Type u_1}
[preorder α]
{s t : set α} :
s.ord_connected → t.ord_connected → (s ∩ t).ord_connected
theorem
set.ord_connected.dual
{α : Type u_1}
[preorder α]
{s : set α} :
s.ord_connected → s.ord_connected
theorem
set.ord_connected_sInter
{α : Type u_1}
[preorder α]
{S : set (set α)} :
(∀ (s : set α), s ∈ S → s.ord_connected) → (⋂₀S).ord_connected
theorem
set.ord_connected_Inter
{α : Type u_1}
[preorder α]
{ι : Sort u_2}
{s : ι → set α} :
(∀ (i : ι), (s i).ord_connected) → (⋂ (i : ι), s i).ord_connected
theorem
set.ord_connected_bInter
{α : Type u_1}
[preorder α]
{ι : Sort u_2}
{p : ι → Prop}
{s : Π (i : ι), p i → set α} :
(∀ (i : ι) (hi : p i), (s i hi).ord_connected) → (⋂ (i : ι) (hi : p i), s i hi).ord_connected
theorem
set.ord_connected_interval
{β : Type u_2}
[decidable_linear_order β]
{a b : β} :
(set.interval a b).ord_connected
theorem
set.ord_connected.interval_subset
{β : Type u_2}
[decidable_linear_order β]
{s : set β}
(hs : s.ord_connected)
⦃x : β⦄
(hx : x ∈ s)
⦃y : β⦄ :
y ∈ s → set.interval x y ⊆ s
theorem
set.ord_connected_iff_interval_subset
{β : Type u_2}
[decidable_linear_order β]
{s : set β} :
s.ord_connected ↔ ∀ ⦃x : β⦄, x ∈ s → ∀ ⦃y : β⦄, y ∈ s → set.interval x y ⊆ s