Mathlib.Order.Interval.Set.OrdConnected

Set.OrdConnected.out theorem

(h : OrdConnected s) : ∀ ⦃x⦄ (_ : x ∈ s) ⦃y⦄ (_ : y ∈ s), Icc x y ⊆ s

Full source

theorem OrdConnected.out (h : OrdConnected s) : ∀ ⦃x⦄ (_ : x ∈ s) ⦃y⦄ (_ : y ∈ s), IccIcc x y ⊆ s :=
  h.1

Order-Connected Sets Contain Intervals

Informal description

If a set $s$ in a linearly ordered type $\alpha$ is order-connected, then for any two elements $x, y \in s$, the closed interval $[x, y]$ is contained in $s$.

Set.ordConnected_def theorem

: OrdConnected s ↔ ∀ ⦃x⦄ (_ : x ∈ s) ⦃y⦄ (_ : y ∈ s), Icc x y ⊆ s

Full source

theorem ordConnected_def : OrdConnectedOrdConnected s ↔ ∀ ⦃x⦄ (_ : x ∈ s) ⦃y⦄ (_ : y ∈ s), Icc x y ⊆ s :=
  ⟨fun h => h.1, fun h => ⟨h⟩⟩

Characterization of Order-Connected Sets via Closed Intervals

Informal description

A set $s$ in a partially ordered type $\alpha$ is order-connected if and only if for any two elements $x, y \in s$, the closed interval $[x, y]$ is contained in $s$.

Set.ordConnected_iff theorem

: OrdConnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Icc x y ⊆ s

Full source

/-- It suffices to prove `[[x, y]] ⊆ s` for `x y ∈ s`, `x ≤ y`. -/
theorem ordConnected_iff : OrdConnectedOrdConnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Icc x y ⊆ s :=
  ordConnected_def.trans
    ⟨fun hs _ hx _ hy _ => hs hx hy, fun H x hx y hy _ hz => H x hx y hy (le_trans hz.1 hz.2) hz⟩

Characterization of Order-Connected Sets via Closed Intervals for Ordered Pairs

Informal description

A set $s$ in a partially ordered type $\alpha$ is order-connected if and only if for any two elements $x, y \in s$ with $x \leq y$, the closed interval $[x, y]$ is contained in $s$.

Set.ordConnected_of_Ioo theorem

{α : Type*} [PartialOrder α] {s : Set α} (hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s) : OrdConnected s

Full source

theorem ordConnected_of_Ioo {α : Type*} [PartialOrder α] {s : Set α}
    (hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s) : OrdConnected s := by
  rw [ordConnected_iff]
  intro x hx y hy hxy
  rcases eq_or_lt_of_le hxy with (rfl | hxy'); · simpa
  rw [← Ioc_insert_left hxy, ← Ioo_insert_right hxy']
  exact insert_subset_iff.2 ⟨hx, insert_subset_iff.2 ⟨hy, hs x hx y hy hxy'⟩⟩

Order-Connectedness via Open Intervals

Informal description

Let $\alpha$ be a partially ordered type and $s$ a subset of $\alpha$. If for any two elements $x, y \in s$ with $x < y$, the open interval $(x, y)$ is contained in $s$, then $s$ is order-connected.

Set.OrdConnected.preimage_mono theorem

{f : β → α} (hs : OrdConnected s) (hf : Monotone f) : OrdConnected (f ⁻¹' s)

Full source

theorem OrdConnected.preimage_mono {f : β → α} (hs : OrdConnected s) (hf : Monotone f) :
    OrdConnected (f ⁻¹' s) :=
  ⟨fun _ hx _ hy _ hz => hs.out hx hy ⟨hf hz.1, hf hz.2⟩⟩

Preimage of Order-Connected Set under Monotone Function is Order-Connected

Informal description

Let $f : \beta \to \alpha$ be a monotone function between partially ordered sets. If a set $s \subseteq \alpha$ is order-connected, then its preimage $f^{-1}(s) \subseteq \beta$ is also order-connected.

Set.OrdConnected.preimage_anti theorem

{f : β → α} (hs : OrdConnected s) (hf : Antitone f) : OrdConnected (f ⁻¹' s)

Full source

theorem OrdConnected.preimage_anti {f : β → α} (hs : OrdConnected s) (hf : Antitone f) :
    OrdConnected (f ⁻¹' s) :=
  ⟨fun _ hx _ hy _ hz => hs.out hy hx ⟨hf hz.2, hf hz.1⟩⟩

Preimage of Order-Connected Set under Antitone Function is Order-Connected

Informal description

Let $f : \beta \to \alpha$ be an antitone function between partially ordered sets. If a set $s \subseteq \alpha$ is order-connected, then its preimage $f^{-1}(s) \subseteq \beta$ is also order-connected.

Set.Icc_subset theorem

(s : Set α) [hs : OrdConnected s] {x y} (hx : x ∈ s) (hy : y ∈ s) : Icc x y ⊆ s

Full source

protected theorem Icc_subset (s : Set α) [hs : OrdConnected s] {x y} (hx : x ∈ s) (hy : y ∈ s) :
    IccIcc x y ⊆ s :=
  hs.out hx hy

Closed Interval Subset of Order-Connected Set

Informal description

For any order-connected set $s$ in a linearly ordered type $\alpha$, and for any two elements $x, y \in s$, the closed interval $[x, y]$ is contained in $s$.

OrderEmbedding.image_Icc theorem

(e : α ↪o β) (he : OrdConnected (range e)) (x y : α) : e '' Icc x y = Icc (e x) (e y)

Full source

theorem image_Icc (e : α ↪o β) (he : OrdConnected (range e)) (x y : α) :
    e '' Icc x y = Icc (e x) (e y) := by
  rw [← e.preimage_Icc, image_preimage_eq_inter_range, inter_eq_left.2 (he.out ⟨_, rfl⟩ ⟨_, rfl⟩)]

Image of Closed Interval under Order Embedding with Order-Connected Range

Informal description

Let $e : \alpha \hookrightarrow \beta$ be an order embedding between linearly ordered sets $\alpha$ and $\beta$, and suppose the range of $e$ is order-connected (i.e., for any two points in the range, the interval between them is also contained in the range). Then for any $x, y \in \alpha$, the image under $e$ of the closed interval $[x, y]$ is equal to the closed interval $[e(x), e(y)]$ in $\beta$. That is, $$ e\big([x, y]\big) = [e(x), e(y)]. $$

OrderEmbedding.image_Ico theorem

(e : α ↪o β) (he : OrdConnected (range e)) (x y : α) : e '' Ico x y = Ico (e x) (e y)

Full source

theorem image_Ico (e : α ↪o β) (he : OrdConnected (range e)) (x y : α) :
    e '' Ico x y = Ico (e x) (e y) := by
  rw [← e.preimage_Ico, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ico_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]

Image of Closed-Open Interval under Order Embedding with Order-Connected Range

Informal description

Let $e : \alpha \hookrightarrow \beta$ be an order embedding between linearly ordered sets $\alpha$ and $\beta$, and suppose the range of $e$ is order-connected (i.e., for any two points in the range, the interval between them is also contained in the range). Then for any $x, y \in \alpha$, the image under $e$ of the closed-open interval $[x, y)$ is equal to the closed-open interval $[e(x), e(y))$ in $\beta$. That is, $$ e\big([x, y)\big) = [e(x), e(y)). $$

OrderEmbedding.image_Ioc theorem

(e : α ↪o β) (he : OrdConnected (range e)) (x y : α) : e '' Ioc x y = Ioc (e x) (e y)

Full source

theorem image_Ioc (e : α ↪o β) (he : OrdConnected (range e)) (x y : α) :
    e '' Ioc x y = Ioc (e x) (e y) := by
  rw [← e.preimage_Ioc, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ioc_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]

Image of Open-Closed Interval under Order Embedding with Order-Connected Range

Informal description

Let $e : \alpha \hookrightarrow \beta$ be an order embedding between linearly ordered sets $\alpha$ and $\beta$, and suppose the range of $e$ is order-connected. Then for any $x, y \in \alpha$, the image under $e$ of the open-closed interval $(x, y]$ is equal to the open-closed interval $(e(x), e(y)]$ in $\beta$. That is, $$ e\big((x, y]\big) = (e(x), e(y)]. $$

OrderEmbedding.image_Ioo theorem

(e : α ↪o β) (he : OrdConnected (range e)) (x y : α) : e '' Ioo x y = Ioo (e x) (e y)

Full source

theorem image_Ioo (e : α ↪o β) (he : OrdConnected (range e)) (x y : α) :
    e '' Ioo x y = Ioo (e x) (e y) := by
  rw [← e.preimage_Ioo, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ioo_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]

Image of Open Interval under Order Embedding with Order-Connected Range

Informal description

Let $e : \alpha \hookrightarrow \beta$ be an order embedding between linearly ordered sets $\alpha$ and $\beta$, and suppose the range of $e$ is order-connected. Then for any $x, y \in \alpha$, the image under $e$ of the open interval $(x, y)$ is equal to the open interval $(e(x), e(y))$ in $\beta$. That is, $$ e\big((x, y)\big) = (e(x), e(y)). $$

Set.image_subtype_val_Icc theorem

{s : Set α} [OrdConnected s] (x y : s) : Subtype.val '' Icc x y = Icc x.1 y

Full source

@[simp]
lemma image_subtype_val_Icc {s : Set α} [OrdConnected s] (x y : s) :
    Subtype.valSubtype.val '' Icc x y = Icc x.1 y :=
  (OrderEmbedding.subtype (· ∈ s)).image_Icc (by simpa) x y

Image of Closed Interval under Inclusion of Order-Connected Subset

Informal description

Let $s$ be an order-connected subset of a linearly ordered type $\alpha$, and let $x, y \in s$. Then the image of the closed interval $[x, y]$ under the canonical inclusion map $\text{Subtype.val} : s \to \alpha$ is equal to the closed interval $[x.1, y.1]$ in $\alpha$. That is, $$ \text{Subtype.val}\big([x, y]\big) = [x.1, y.1]. $$

Set.image_subtype_val_Ico theorem

{s : Set α} [OrdConnected s] (x y : s) : Subtype.val '' Ico x y = Ico x.1 y

Full source

@[simp]
lemma image_subtype_val_Ico {s : Set α} [OrdConnected s] (x y : s) :
    Subtype.valSubtype.val '' Ico x y = Ico x.1 y :=
  (OrderEmbedding.subtype (· ∈ s)).image_Ico (by simpa) x y

Image of Closed-Open Interval in Order-Connected Set under Inclusion

Informal description

Let $s$ be an order-connected subset of a linearly ordered type $\alpha$, and let $x, y \in s$. Then the image of the closed-open interval $[x, y)$ under the canonical inclusion map $\text{val} : s \to \alpha$ is equal to the closed-open interval $[x.1, y.1)$ in $\alpha$. That is, $$ \text{val}\big([x, y)\big) = [x.1, y.1). $$

Set.image_subtype_val_Ioc theorem

{s : Set α} [OrdConnected s] (x y : s) : Subtype.val '' Ioc x y = Ioc x.1 y

Full source

@[simp]
lemma image_subtype_val_Ioc {s : Set α} [OrdConnected s] (x y : s) :
    Subtype.valSubtype.val '' Ioc x y = Ioc x.1 y :=
  (OrderEmbedding.subtype (· ∈ s)).image_Ioc (by simpa) x y

Image of Open-Closed Interval in Order-Connected Set via Subtype Inclusion

Informal description

Let $s$ be an order-connected subset of a linearly ordered type $\alpha$, and let $x, y \in s$. Then the image of the open-closed interval $(x, y]$ under the canonical inclusion map $\text{val} : s \hookrightarrow \alpha$ is equal to the open-closed interval $(x.1, y.1]$ in $\alpha$. That is, $$ \text{val}\big((x, y]\big) = (x.1, y.1]. $$

Set.image_subtype_val_Ioo theorem

{s : Set α} [OrdConnected s] (x y : s) : Subtype.val '' Ioo x y = Ioo x.1 y

Full source

@[simp]
lemma image_subtype_val_Ioo {s : Set α} [OrdConnected s] (x y : s) :
    Subtype.valSubtype.val '' Ioo x y = Ioo x.1 y :=
  (OrderEmbedding.subtype (· ∈ s)).image_Ioo (by simpa) x y

Image of Open Interval in Order-Connected Set via Inclusion

Informal description

Let $s$ be an order-connected subset of a linearly ordered type $\alpha$, and let $x, y \in s$. Then the image of the open interval $(x, y)$ under the canonical inclusion map $\text{val} : s \hookrightarrow \alpha$ is equal to the open interval $(x.1, y.1)$ in $\alpha$. That is, $$ \text{val}\big((x, y)\big) = (x.1, y.1). $$

Set.OrdConnected.inter theorem

{s t : Set α} (hs : OrdConnected s) (ht : OrdConnected t) : OrdConnected (s ∩ t)

Full source

theorem OrdConnected.inter {s t : Set α} (hs : OrdConnected s) (ht : OrdConnected t) :
    OrdConnected (s ∩ t) :=
  ⟨fun _ hx _ hy => subset_inter (hs.out hx.1 hy.1) (ht.out hx.2 hy.2)⟩

Intersection of Order-Connected Sets is Order-Connected

Informal description

Let $s$ and $t$ be order-connected sets in a linearly ordered type $\alpha$. Then their intersection $s \cap t$ is also order-connected.

Set.OrdConnected.inter' instance

{s t : Set α} [OrdConnected s] [OrdConnected t] : OrdConnected (s ∩ t)

Full source

instance OrdConnected.inter' {s t : Set α} [OrdConnected s] [OrdConnected t] :
    OrdConnected (s ∩ t) :=
  OrdConnected.inter ‹_› ‹_›

Intersection of Order-Connected Sets is Order-Connected

Informal description

For any two order-connected sets $s$ and $t$ in a linearly ordered type $\alpha$, their intersection $s \cap t$ is also order-connected.

Set.OrdConnected.dual theorem

{s : Set α} (hs : OrdConnected s) : OrdConnected (OrderDual.ofDual ⁻¹' s)

Full source

theorem OrdConnected.dual {s : Set α} (hs : OrdConnected s) :
    OrdConnected (OrderDual.ofDualOrderDual.ofDual ⁻¹' s) :=
  ⟨fun _ hx _ hy _ hz => hs.out hy hx ⟨hz.2, hz.1⟩⟩

Order-Connected Sets are Preserved Under Order Duality

Informal description

Let $s$ be an order-connected set in a linearly ordered type $\alpha$. Then the preimage of $s$ under the order-reversing map $\text{OrderDual.ofDual} : \alpha^{\text{dual}} \to \alpha$ is also order-connected in the dual order $\alpha^{\text{dual}}$.

Set.ordConnected_dual theorem

{s : Set α} : OrdConnected (OrderDual.ofDual ⁻¹' s) ↔ OrdConnected s

Full source

theorem ordConnected_dual {s : Set α} : OrdConnectedOrdConnected (OrderDual.ofDual ⁻¹' s) ↔ OrdConnected s :=
  ⟨fun h => by simpa only [ordConnected_def] using h.dual, fun h => h.dual⟩

Order-Connectedness is Equivalent Under Order Duality

Informal description

For any set $s$ in a linearly ordered type $\alpha$, the preimage of $s$ under the order-reversing map $\text{OrderDual.ofDual} : \alpha^{\text{dual}} \to \alpha$ is order-connected if and only if $s$ itself is order-connected.

Set.ordConnected_sInter theorem

{S : Set (Set α)} (hS : ∀ s ∈ S, OrdConnected s) : OrdConnected (⋂₀ S)

Full source

theorem ordConnected_sInter {S : Set (Set α)} (hS : ∀ s ∈ S, OrdConnected s) :
    OrdConnected (⋂₀ S) :=
  ⟨fun _x hx _y hy _z hz s hs => (hS s hs).out (hx s hs) (hy s hs) hz⟩

Intersection of Order-Connected Sets is Order-Connected

Informal description

Let $\alpha$ be a type with a linear order, and let $S$ be a collection of subsets of $\alpha$. If every set $s \in S$ is order-connected (i.e., for any $x, y \in s$, the interval $[x, y]$ is contained in $s$), then the intersection $\bigcap S$ is also order-connected.

Set.ordConnected_iInter theorem

{ι : Sort*} {s : ι → Set α} (hs : ∀ i, OrdConnected (s i)) : OrdConnected (⋂ i, s i)

Full source

theorem ordConnected_iInter {ι : Sort*} {s : ι → Set α} (hs : ∀ i, OrdConnected (s i)) :
    OrdConnected (⋂ i, s i) :=
  ordConnected_sInter <| forall_mem_range.2 hs

Intersection of a Family of Order-Connected Sets is Order-Connected

Informal description

Let $\alpha$ be a type with a linear order, and let $\{s_i\}_{i \in \iota}$ be a family of subsets of $\alpha$ indexed by some type $\iota$. If each set $s_i$ is order-connected (i.e., for any $x, y \in s_i$, the interval $[x, y]$ is contained in $s_i$), then the intersection $\bigcap_{i \in \iota} s_i$ is also order-connected.

Set.ordConnected_iInter' instance

{ι : Sort*} {s : ι → Set α} [∀ i, OrdConnected (s i)] : OrdConnected (⋂ i, s i)

Full source

instance ordConnected_iInter' {ι : Sort*} {s : ι → Set α} [∀ i, OrdConnected (s i)] :
    OrdConnected (⋂ i, s i) :=
  ordConnected_iInter ‹_›

Intersection of Order-Connected Sets is Order-Connected

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ in a linearly ordered type $\alpha$, if each $s_i$ is order-connected (i.e., contains the interval $[x, y]$ for any $x, y \in s_i$), then the intersection $\bigcap_{i \in \iota} s_i$ is also order-connected.

Set.ordConnected_biInter theorem

 {ι : Sort*} {p : ι → Prop} {s : ∀ i, p i → Set α} (hs : ∀ i hi, OrdConnected (s i hi)) :
  OrdConnected (⋂ (i) (hi), s i hi)

Full source

theorem ordConnected_biInter {ι : Sort*} {p : ι → Prop} {s : ∀ i, p i → Set α}
    (hs : ∀ i hi, OrdConnected (s i hi)) : OrdConnected (⋂ (i) (hi), s i hi) :=
  ordConnected_iInter fun i => ordConnected_iInter <| hs i

Intersection of Conditionally Indexed Order-Connected Sets is Order-Connected

Informal description

Let $\alpha$ be a type with a linear order, and let $\{s_i\}_{i \in \iota}$ be a family of subsets of $\alpha$ indexed by some type $\iota$ with a predicate $p : \iota \to \mathrm{Prop}$. If for each $i \in \iota$ satisfying $p(i)$, the set $s_i$ is order-connected (i.e., for any $x, y \in s_i$, the interval $[x, y]$ is contained in $s_i$), then the intersection $\bigcap_{i \in \iota, p(i)} s_i$ is also order-connected.

Set.ordConnected_pi theorem

 {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] {s : Set ι} {t : ∀ i, Set (α i)} (h : ∀ i ∈ s, OrdConnected (t i)) :
  OrdConnected (s.pi t)

Full source

theorem ordConnected_pi {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] {s : Set ι}
    {t : ∀ i, Set (α i)} (h : ∀ i ∈ s, OrdConnected (t i)) : OrdConnected (s.pi t) :=
  ⟨fun _ hx _ hy _ hz i hi => (h i hi).out (hx i hi) (hy i hi) ⟨hz.1 i, hz.2 i⟩⟩

Product of Order-Connected Sets is Order-Connected

Informal description

Let $\{ \alpha_i \}_{i \in \iota}$ be a family of preordered types, and let $s \subseteq \iota$ be a subset of indices. For each $i \in s$, let $t_i \subseteq \alpha_i$ be an order-connected set. Then the product set $\prod_{i \in s} t_i$ is order-connected in the product space $\prod_{i \in \iota} \alpha_i$ with the product order. That is, for any two points $x, y \in \prod_{i \in s} t_i$, the interval $[x, y]$ is contained in $\prod_{i \in s} t_i$.

Set.ordConnected_pi' instance

 {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] {s : Set ι} {t : ∀ i, Set (α i)} [h : ∀ i, OrdConnected (t i)] :
  OrdConnected (s.pi t)

Full source

instance ordConnected_pi' {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] {s : Set ι}
    {t : ∀ i, Set (α i)} [h : ∀ i, OrdConnected (t i)] : OrdConnected (s.pi t) :=
  ordConnected_pi fun i _ => h i

Product of Order-Connected Sets is Order-Connected

Informal description

For a family of preordered types $\{\alpha_i\}_{i \in \iota}$ and a subset $s \subseteq \iota$, if each set $t_i \subseteq \alpha_i$ is order-connected, then the product set $\prod_{i \in s} t_i$ is order-connected in the product space $\prod_{i \in \iota} \alpha_i$ with the product order. That is, for any two points $x, y \in \prod_{i \in s} t_i$, the interval $[x, y]$ is contained in $\prod_{i \in s} t_i$.

Set.ordConnected_Ici theorem

{a : α} : OrdConnected (Ici a)

Full source

@[instance]
theorem ordConnected_Ici {a : α} : OrdConnected (Ici a) :=
  ⟨fun _ hx _ _ _ hz => le_trans hx hz.1⟩

Upper Closure is Order Connected

Informal description

For any element $a$ in a preorder $\alpha$, the set $\{x \in \alpha \mid a \leq x\}$ (the upper closure of $a$) is order connected. That is, for any two elements $x, y$ in this set, the entire interval $[x, y]$ is also contained in the set.

Set.ordConnected_Iic theorem

{a : α} : OrdConnected (Iic a)

Full source

@[instance]
theorem ordConnected_Iic {a : α} : OrdConnected (Iic a) :=
  ⟨fun _ _ _ hy _ hz => le_trans hz.2 hy⟩

Lower Set is Order-Connected

Informal description

For any element $a$ in a preorder $\alpha$, the lower set $Iic(a) = \{x \in \alpha \mid x \leq a\}$ is order-connected. That is, for any $x, y \in Iic(a)$, the interval $[x, y]$ is entirely contained in $Iic(a)$.

Set.ordConnected_Ioi theorem

{a : α} : OrdConnected (Ioi a)

Full source

@[instance]
theorem ordConnected_Ioi {a : α} : OrdConnected (Ioi a) :=
  ⟨fun _ hx _ _ _ hz => lt_of_lt_of_le hx hz.1⟩

Open upper interval $(a, \infty)$ is order-connected

Informal description

For any element $a$ in a linearly ordered type $\alpha$, the open interval $(a, \infty)$ is order-connected. That is, for any $x, y \in (a, \infty)$, the closed interval $[x, y]$ is entirely contained in $(a, \infty)$.

Set.ordConnected_Iio theorem

{a : α} : OrdConnected (Iio a)

Full source

@[instance]
theorem ordConnected_Iio {a : α} : OrdConnected (Iio a) :=
  ⟨fun _ _ _ hy _ hz => lt_of_le_of_lt hz.2 hy⟩

Order-connectedness of the open interval $(-\infty, a)$

Informal description

For any element $a$ in a linearly ordered type $\alpha$, the open interval $(-\infty, a)$ is order-connected. That is, for any two elements $x, y \in (-\infty, a)$, the entire closed interval $[x, y]$ is contained in $(-\infty, a)$.

Set.ordConnected_Icc theorem

{a b : α} : OrdConnected (Icc a b)

Full source

@[instance]
theorem ordConnected_Icc {a b : α} : OrdConnected (Icc a b) :=
  ordConnected_Ici.inter ordConnected_Iic

Closed Interval is Order-Connected

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$, the closed interval $[a, b] = \{x \in \alpha \mid a \leq x \leq b\}$ is order-connected. That is, for any two elements $x, y \in [a, b]$, the entire interval $[x, y]$ is contained in $[a, b]$.

Set.ordConnected_Ico theorem

{a b : α} : OrdConnected (Ico a b)

Full source

@[instance]
theorem ordConnected_Ico {a b : α} : OrdConnected (Ico a b) :=
  ordConnected_Ici.inter ordConnected_Iio

Order-connectedness of the half-open interval $[a, b)$

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$, the half-open interval $[a, b) = \{x \in \alpha \mid a \leq x < b\}$ is order-connected. That is, for any two elements $x, y \in [a, b)$, the entire interval $[x, y]$ is contained in $[a, b)$.

Set.ordConnected_Ioc theorem

{a b : α} : OrdConnected (Ioc a b)

Full source

@[instance]
theorem ordConnected_Ioc {a b : α} : OrdConnected (Ioc a b) :=
  ordConnected_Ioi.inter ordConnected_Iic

Order-connectedness of the half-open interval $(a, b]$

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$, the half-open interval $(a, b] = \{x \in \alpha \mid a < x \leq b\}$ is order-connected. That is, for any two elements $x, y \in (a, b]$, the entire closed interval $[x, y]$ is contained in $(a, b]$.

Set.ordConnected_Ioo theorem

{a b : α} : OrdConnected (Ioo a b)

Full source

@[instance]
theorem ordConnected_Ioo {a b : α} : OrdConnected (Ioo a b) :=
  ordConnected_Ioi.inter ordConnected_Iio

Order-connectedness of the open interval $(a, b)$

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$, the open interval $(a, b) = \{x \in \alpha \mid a < x < b\}$ is order-connected. That is, for any two elements $x, y \in (a, b)$, the entire closed interval $[x, y]$ is contained in $(a, b)$.

Set.ordConnected_singleton theorem

{α : Type*} [PartialOrder α] {a : α} : OrdConnected ({ a } : Set α)

Full source

@[instance]
theorem ordConnected_singleton {α : Type*} [PartialOrder α] {a : α} :
    OrdConnected ({a} : Set α) := by
  rw [← Icc_self]
  exact ordConnected_Icc

Order-connectedness of Singleton Sets

Informal description

For any element $a$ in a partially ordered type $\alpha$, the singleton set $\{a\}$ is order-connected. That is, for any two elements $x, y \in \{a\}$, the closed interval $[x, y]$ is contained in $\{a\}$.

Set.ordConnected_empty theorem

: OrdConnected (∅ : Set α)

Full source

@[instance]
theorem ordConnected_empty : OrdConnected (∅ : Set α) :=
  ⟨fun _ => False.elim⟩

Empty Set is Order Connected

Informal description

The empty set is order connected in any partially ordered type $\alpha$.

Set.ordConnected_univ theorem

: OrdConnected (univ : Set α)

Full source

@[instance]
theorem ordConnected_univ : OrdConnected (univ : Set α) :=
  ⟨fun _ _ _ _ => subset_univ _⟩

Universal Set is Order-Connected

Informal description

The universal set `univ : Set α` is order-connected. That is, for any two elements `x y ∈ univ`, the closed interval `[[x, y]]` is entirely contained in `univ`.

Set.instDenselyOrdered instance

[DenselyOrdered α] {s : Set α} [hs : OrdConnected s] : DenselyOrdered s

Full source

/-- In a dense order `α`, the subtype from an `OrdConnected` set is also densely ordered. -/
instance instDenselyOrdered [DenselyOrdered α] {s : Set α} [hs : OrdConnected s] :
    DenselyOrdered s :=
  ⟨fun a b (h : (a : α) < b) =>
    let ⟨x, H⟩ := exists_between h
    ⟨⟨x, (hs.out a.2 b.2) (Ioo_subset_Icc_self H)⟩, H⟩⟩

Order-Connected Subsets of Densely Ordered Types are Densely Ordered

Informal description

For any densely ordered type $\alpha$ and an order-connected subset $s \subseteq \alpha$, the subtype $s$ is also densely ordered.

Set.ordConnected_preimage theorem

 {F : Type*} [FunLike F α β] [OrderHomClass F α β] (f : F) {s : Set β} [hs : OrdConnected s] : OrdConnected (f ⁻¹' s)

Full source

@[instance]
theorem ordConnected_preimage {F : Type*} [FunLike F α β] [OrderHomClass F α β] (f : F)
    {s : Set β} [hs : OrdConnected s] : OrdConnected (f ⁻¹' s) :=
  ⟨fun _ hx _ hy _ hz => hs.out hx hy ⟨OrderHomClass.mono _ hz.1, OrderHomClass.mono _ hz.2⟩⟩

Preimage of Order-Connected Set under Order-Preserving Function is Order-Connected

Informal description

Let $\alpha$ and $\beta$ be types with a function-like structure $F$ between them, where $F$ preserves the order (i.e., $F$ is an order homomorphism). If $s \subseteq \beta$ is an order-connected set, then the preimage $f^{-1}(s) \subseteq \alpha$ under any order-preserving function $f \in F$ is also order-connected.

Set.ordConnected_image theorem

 {E : Type*} [EquivLike E α β] [OrderIsoClass E α β] (e : E) {s : Set α} [hs : OrdConnected s] : OrdConnected (e '' s)

Full source

@[instance]
theorem ordConnected_image {E : Type*} [EquivLike E α β] [OrderIsoClass E α β] (e : E) {s : Set α}
    [hs : OrdConnected s] : OrdConnected (e '' s) := by
  erw [(e : α ≃o β).image_eq_preimage]
  apply ordConnected_preimage (e : α ≃o β).symm

Image of Order-Connected Set under Order Isomorphism is Order-Connected

Informal description

Let $\alpha$ and $\beta$ be types equipped with order structures, and let $E$ be a type of equivalences between $\alpha$ and $\beta$ that preserve the order (i.e., order isomorphisms). For any order-connected set $s \subseteq \alpha$ and any order isomorphism $e \in E$, the image $e(s) \subseteq \beta$ is also order-connected.

Set.ordConnected_range theorem

{E : Type*} [EquivLike E α β] [OrderIsoClass E α β] (e : E) : OrdConnected (range e)

Full source

@[instance]
theorem ordConnected_range {E : Type*} [EquivLike E α β] [OrderIsoClass E α β] (e : E) :
    OrdConnected (range e) := by
  simp_rw [← image_univ]
  exact ordConnected_image (e : α ≃o β)

Range of Order Isomorphism is Order-Connected

Informal description

Let $\alpha$ and $\beta$ be types equipped with order structures, and let $E$ be a type of equivalences between $\alpha$ and $\beta$ that preserve the order (i.e., order isomorphisms). For any order isomorphism $e \in E$, the range of $e$ is order-connected. That is, for any two elements $x, y$ in the range of $e$, the closed interval $[[x, y]]$ is entirely contained in the range of $e$.

Set.dual_ordConnected_iff theorem

{s : Set α} : OrdConnected (ofDual ⁻¹' s) ↔ OrdConnected s

Full source

@[simp]
theorem dual_ordConnected_iff {s : Set α} : OrdConnectedOrdConnected (ofDual ⁻¹' s) ↔ OrdConnected s := by
  simp_rw [ordConnected_def, toDual.surjective.forall, Icc_toDual, Subtype.forall']
  exact forall_swap

Order Connectedness under Order Duality

Informal description

A set $s$ in a partially ordered set $\alpha$ is order connected if and only if its preimage under the order dual operation (i.e., the set obtained by reversing the order relation on $\alpha$) is order connected.

Set.dual_ordConnected theorem

{s : Set α} [OrdConnected s] : OrdConnected (ofDual ⁻¹' s)

Full source

@[instance]
theorem dual_ordConnected {s : Set α} [OrdConnected s] : OrdConnected (ofDualofDual ⁻¹' s) :=
  dual_ordConnected_iff.2 ‹_›

Order Connectedness Preserved under Order Duality

Informal description

Let $s$ be an order connected set in a partially ordered set $\alpha$. Then the preimage of $s$ under the order dual operation (i.e., the set obtained by reversing the order relation on $\alpha$) is also order connected.

IsAntichain.ordConnected theorem

(hs : IsAntichain (· ≤ ·) s) : s.OrdConnected

Full source

protected theorem _root_.IsAntichain.ordConnected (hs : IsAntichain (· ≤ ·) s) : s.OrdConnected :=
  ⟨fun x hx y hy z hz => by
    obtain rfl := hs.eq hx hy (hz.1.trans hz.2)
    rw [Icc_self, mem_singleton_iff] at hz
    rwa [hz]⟩

Antichains are Order Connected

Informal description

If a set $s$ in a partially ordered set is an antichain (i.e., no two distinct elements in $s$ are comparable under the order relation $\leq$), then $s$ is order connected. This means that for any two elements $x, y \in s$, the interval $[[x, y]]$ is contained in $s$.

Set.ordConnected_inter_Icc_of_subset theorem

(h : Ioo x y ⊆ s) : OrdConnected (s ∩ Icc x y)

Full source

lemma ordConnected_inter_Icc_of_subset (h : IooIoo x y ⊆ s) : OrdConnected (s ∩ Icc x y) :=
  ordConnected_of_Ioo fun _u ⟨_, hu, _⟩ _v ⟨_, _, hv⟩ _ ↦
    Ioo_subset_Ioo hu hv |>.trans <| subset_inter h Ioo_subset_Icc_self

Order-Connectedness of Intersection with Closed Interval via Open Interval Inclusion

Informal description

Let $\alpha$ be a partially ordered type, $s$ a subset of $\alpha$, and $x, y$ elements of $\alpha$. If the open interval $(x, y)$ is contained in $s$, then the intersection $s \cap [x, y]$ is order-connected.

Set.ordConnected_inter_Icc_iff theorem

(hx : x ∈ s) (hy : y ∈ s) : OrdConnected (s ∩ Icc x y) ↔ Ioo x y ⊆ s

Full source

lemma ordConnected_inter_Icc_iff (hx : x ∈ s) (hy : y ∈ s) :
    OrdConnectedOrdConnected (s ∩ Icc x y) ↔ Ioo x y ⊆ s := by
  refine ⟨fun h ↦ Ioo_subset_Icc_self.trans fun z hz ↦ ?_, ordConnected_inter_Icc_of_subset⟩
  have hxy : x ≤ y := hz.1.trans hz.2
  exact h.out ⟨hx, left_mem_Icc.2 hxy⟩ ⟨hy, right_mem_Icc.2 hxy⟩ hz |>.1

Order-Connectedness of Intersection with Closed Interval via Open Interval Inclusion Criterion

Informal description

Let $\alpha$ be a partially ordered type, $s$ a subset of $\alpha$, and $x, y$ elements of $s$. The intersection $s \cap [x, y]$ is order-connected if and only if the open interval $(x, y)$ is contained in $s$.

Set.not_ordConnected_inter_Icc_iff theorem

(hx : x ∈ s) (hy : y ∈ s) : ¬OrdConnected (s ∩ Icc x y) ↔ ∃ z ∉ s, z ∈ Ioo x y

Full source

lemma not_ordConnected_inter_Icc_iff (hx : x ∈ s) (hy : y ∈ s) :
    ¬ OrdConnected (s ∩ Icc x y)¬ OrdConnected (s ∩ Icc x y) ↔ ∃ z ∉ s, z ∈ Ioo x y := by
  simp_rw [ordConnected_inter_Icc_iff hx hy, subset_def, not_forall, exists_prop, and_comm]

Non-Order-Connectedness Criterion via Missing Point in Open Interval

Informal description

Let $\alpha$ be a partially ordered type, $s$ a subset of $\alpha$, and $x, y$ elements of $s$. The intersection $s \cap [x, y]$ is not order-connected if and only if there exists an element $z$ in the open interval $(x, y)$ that does not belong to $s$.

Set.ordConnected_uIcc theorem

{a b : α} : OrdConnected [[a, b]]

Full source

@[instance]
theorem ordConnected_uIcc {a b : α} : OrdConnected [[a, b]] :=
  ordConnected_Icc

Closed Interval Between Two Points is Order-Connected

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$, the interval $[[a, b]]$ (the closed interval from $\min(a,b)$ to $\max(a,b)$) is order-connected. That is, for any two elements $x, y \in [[a, b]]$, the entire interval $[x, y]$ is contained in $[[a, b]]$.

Set.ordConnected_uIoc theorem

{a b : α} : OrdConnected (Ι a b)

Full source

@[instance]
theorem ordConnected_uIoc {a b : α} : OrdConnected (Ι a b) :=
  ordConnected_Ioc

Order-connectedness of the open-closed interval $\text{Ι}(a, b)$

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$, the open-closed interval $\text{Ι}(a, b) = (\min(a,b), \max(a,b)]$ is order-connected. That is, for any two elements $x, y \in \text{Ι}(a, b)$, the entire closed interval $[x, y]$ is contained in $\text{Ι}(a, b)$.

Set.OrdConnected.uIcc_subset theorem

(hs : OrdConnected s) ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s) : [[x, y]] ⊆ s

Full source

theorem OrdConnected.uIcc_subset (hs : OrdConnected s) ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s) :
    [[x, y]][[x, y]] ⊆ s :=
  hs.out (min_rec' (· ∈ s) hx hy) (max_rec' (· ∈ s) hx hy)

Order-Connected Sets Contain Closed Intervals

Informal description

If a set $s$ in a linearly ordered type $\alpha$ is order-connected, then for any two elements $x, y \in s$, the closed interval $[x, y]$ is contained in $s$.

Set.OrdConnected.uIoc_subset theorem

(hs : OrdConnected s) ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s) : Ι x y ⊆ s

Full source

theorem OrdConnected.uIoc_subset (hs : OrdConnected s) ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s) :
    ΙΙ x y ⊆ s :=
  Ioc_subset_Icc_self.trans <| hs.uIcc_subset hx hy

Order-Connected Sets Contain Open-Closed Intervals

Informal description

If a set $s$ in a linearly ordered type $\alpha$ is order-connected, then for any two elements $x, y \in s$, the open-closed interval $\text{Ι}(x, y)$ is contained in $s$.

Set.ordConnected_iff_uIcc_subset theorem

: OrdConnected s ↔ ∀ ⦃x⦄ (_ : x ∈ s) ⦃y⦄ (_ : y ∈ s), [[x, y]] ⊆ s

Full source

theorem ordConnected_iff_uIcc_subset :
    OrdConnectedOrdConnected s ↔ ∀ ⦃x⦄ (_ : x ∈ s) ⦃y⦄ (_ : y ∈ s), [[x, y]] ⊆ s :=
  ⟨fun h => h.uIcc_subset, fun H => ⟨fun _ hx _ hy => Icc_subset_uIcc.trans <| H hx hy⟩⟩

Characterization of Order-Connected Sets via Closed Intervals

Informal description

A set $s$ in a linearly ordered type $\alpha$ is order-connected if and only if for any two elements $x, y \in s$, the closed interval $[x, y]$ is contained in $s$.

Set.ordConnected_of_uIcc_subset_left theorem

(h : ∀ y ∈ s, [[x, y]] ⊆ s) : OrdConnected s

Full source

theorem ordConnected_of_uIcc_subset_left (h : ∀ y ∈ s, [[x, y]] ⊆ s) : OrdConnected s :=
  ordConnected_iff_uIcc_subset.2 fun y hy z hz =>
    calc
      [[y, z]] ⊆ [[y, x]] ∪ [[x, z]] := uIcc_subset_uIcc_union_uIcc
      _ = [[x, y]] ∪ [[x, z]] := by rw [uIcc_comm]
      _ ⊆ s := union_subset (h y hy) (h z hz)

Order-Connectedness via Left-Based Closed Intervals

Informal description

Let $s$ be a set in a linearly ordered type $\alpha$ and let $x \in s$. If for every $y \in s$ the closed interval $[x, y]$ is contained in $s$, then $s$ is order-connected.

Set.ordConnected_iff_uIcc_subset_left theorem

(hx : x ∈ s) : OrdConnected s ↔ ∀ ⦃y⦄, y ∈ s → [[x, y]] ⊆ s

Full source

theorem ordConnected_iff_uIcc_subset_left (hx : x ∈ s) :
    OrdConnectedOrdConnected s ↔ ∀ ⦃y⦄, y ∈ s → [[x, y]] ⊆ s :=
  ⟨fun hs => hs.uIcc_subset hx, ordConnected_of_uIcc_subset_left⟩

Characterization of Order-Connected Sets via Left-Based Closed Intervals

Informal description

Let $s$ be a set in a linearly ordered type $\alpha$ and let $x \in s$. Then $s$ is order-connected if and only if for every $y \in s$, the closed interval $[x, y]$ is contained in $s$.

Set.ordConnected_iff_uIcc_subset_right theorem

(hx : x ∈ s) : OrdConnected s ↔ ∀ ⦃y⦄, y ∈ s → [[y, x]] ⊆ s

Full source

theorem ordConnected_iff_uIcc_subset_right (hx : x ∈ s) :
    OrdConnectedOrdConnected s ↔ ∀ ⦃y⦄, y ∈ s → [[y, x]] ⊆ s := by
  simp_rw [ordConnected_iff_uIcc_subset_left hx, uIcc_comm]

Characterization of Order-Connected Sets via Right-Based Closed Intervals

Informal description

Let $s$ be a set in a linearly ordered type $\alpha$ and let $x \in s$. Then $s$ is order-connected if and only if for every $y \in s$, the closed interval $[y, x]$ is contained in $s$.