Order-connected sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 α is a
linear_ordered_field, 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.
@[class]
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 α is a
linear_ordered_field, then this condition is also equivalent to convex α s.
Instances of this typeclass
- set.ord_connected.inter'
- set.ord_connected_Inter'
- set.ord_connected_pi'
- set.ord_connected_Ici
- set.ord_connected_Iic
- set.ord_connected_Ioi
- set.ord_connected_Iio
- set.ord_connected_Icc
- set.ord_connected_Ico
- set.ord_connected_Ioc
- set.ord_connected_Ioo
- set.ord_connected_singleton
- set.ord_connected_empty
- set.ord_connected_univ
- set.ord_connected_preimage
- set.ord_connected_image
- set.ord_connected_range
- set.dual_ord_connected
- set.ord_connected_uIcc
- set.ord_connected_uIoc
theorem
set.ord_connected.out
{α : Type u_1}
[preorder α]
{s : set α}
(h : s.ord_connected)
⦃x : α⦄
(hx : x ∈ s)
⦃y : α⦄
(hy : y ∈ s) :
theorem
set.ord_connected.preimage_mono
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{s : set α}
{f : β → α}
(hs : s.ord_connected)
(hf : monotone f) :
(f ⁻¹' s).ord_connected
theorem
set.ord_connected.preimage_anti
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{s : set α}
{f : β → α}
(hs : s.ord_connected)
(hf : antitone f) :
(f ⁻¹' s).ord_connected
@[protected]
theorem
set.Icc_subset
{α : Type u_1}
[preorder α]
(s : set α)
[hs : s.ord_connected]
{x y : α}
(hx : x ∈ s)
(hy : y ∈ s) :
theorem
set.ord_connected.inter
{α : Type u_1}
[preorder α]
{s t : set α}
(hs : s.ord_connected)
(ht : t.ord_connected) :
(s ∩ t).ord_connected
@[protected, instance]
def
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_sInter
{α : Type u_1}
[preorder α]
{S : set (set α)}
(hS : ∀ (s : set α), s ∈ S → s.ord_connected) :
(⋂₀ S).ord_connected
theorem
set.ord_connected_Inter
{α : Type u_1}
[preorder α]
{ι : Sort u_2}
{s : ι → set α}
(hs : ∀ (i : ι), (s i).ord_connected) :
(⋂ (i : ι), s i).ord_connected
@[protected, instance]
def
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 α}
(hs : ∀ (i : ι) (hi : p i), (s i hi).ord_connected) :
(⋂ (i : ι) (hi : p i), s i hi).ord_connected
@[protected, instance]
def
set.ord_connected_pi'
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), preorder (α i)]
{s : set ι}
{t : Π (i : ι), set (α i)}
[h : ∀ (i : ι), (t i).ord_connected] :
(s.pi t).ord_connected
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[protected, instance]
def
set.densely_ordered
{α : Type u_1}
[preorder α]
[densely_ordered α]
{s : set α}
[hs : s.ord_connected] :
In a dense order α, the subtype from an ord_connected set is also densely ordered.
@[instance]
theorem
set.ord_connected_preimage
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{F : Type u_3}
[order_hom_class F α β]
(f : F)
{s : set β}
[hs : s.ord_connected] :
(⇑f ⁻¹' s).ord_connected
@[instance]
theorem
set.ord_connected_image
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{E : Type u_3}
[order_iso_class E α β]
(e : E)
{s : set α}
[hs : s.ord_connected] :
(⇑e '' s).ord_connected
@[instance]
theorem
set.ord_connected_range
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{E : Type u_3}
[order_iso_class E α β]
(e : E) :
@[simp]
@[instance]
@[protected]
theorem
is_antichain.ord_connected
{α : Type u_1}
[partial_order α]
{s : set α}
(hs : is_antichain has_le.le s) :
@[instance]
theorem
set.ord_connected_uIcc
{α : Type u_1}
[linear_order α]
{a b : α} :
(set.uIcc a b).ord_connected
@[instance]
theorem
set.ord_connected_uIoc
{α : Type u_1}
[linear_order α]
{a b : α} :
(set.uIoc a b).ord_connected
theorem
set.ord_connected.uIcc_subset
{α : Type u_1}
[linear_order α]
{s : set α}
(hs : s.ord_connected)
⦃x : α⦄
(hx : x ∈ s)
⦃y : α⦄
(hy : y ∈ s) :
theorem
set.ord_connected.uIoc_subset
{α : Type u_1}
[linear_order α]
{s : set α}
(hs : s.ord_connected)
⦃x : α⦄
(hx : x ∈ s)
⦃y : α⦄
(hy : y ∈ s) :
theorem
set.ord_connected_of_uIcc_subset_left
{α : Type u_1}
[linear_order α]
{s : set α}
{x : α}
(h : ∀ (y : α), y ∈ s → set.uIcc x y ⊆ s) :
theorem
set.ord_connected_iff_uIcc_subset_left
{α : Type u_1}
[linear_order α]
{s : set α}
{x : α}
(hx : x ∈ s) :
theorem
set.ord_connected_iff_uIcc_subset_right
{α : Type u_1}
[linear_order α]
{s : set α}
{x : α}
(hx : x ∈ s) :