doc-next-gen

Mathlib.Order.SuccPred.CompleteLinearOrder

Module docstring

{"# Relation between IsSuccPrelimit and iSup in (conditionally) complete linear orders.

"}

csSup_mem_of_not_isSuccPrelimit theorem
(hne : s.Nonempty) (hbdd : BddAbove s) (hlim : ¬IsSuccPrelimit (sSup s)) : sSup s ∈ s
Full source 
lemma csSup_mem_of_not_isSuccPrelimit
    (hne : s.Nonempty) (hbdd : BddAbove s) (hlim : ¬ IsSuccPrelimit (sSup s)) : sSupsSup s ∈ s := by
  obtain ⟨y, hy⟩ := not_forall_not.mp hlim
  obtain ⟨i, his, hi⟩ := exists_lt_of_lt_csSup hne hy.lt
  exact eq_of_le_of_not_lt (le_csSup hbdd his) (hy.2 hi) ▸ his
Supremum is in set when not a successor prelimit
Informal description
Let $\alpha$ be a conditionally complete linear order and $s$ a nonempty subset of $\alpha$ that is bounded above. If the supremum $\sup s$ is not a successor prelimit (i.e., $\neg\text{IsSuccPrelimit}(\sup s)$), then $\sup s$ is an element of $s$.
csInf_mem_of_not_isPredPrelimit theorem
(hne : s.Nonempty) (hbdd : BddBelow s) (hlim : ¬IsPredPrelimit (sInf s)) : sInf s ∈ s
Full source 
lemma csInf_mem_of_not_isPredPrelimit
    (hne : s.Nonempty) (hbdd : BddBelow s) (hlim : ¬ IsPredPrelimit (sInf s)) : sInfsInf s ∈ s := by
  obtain ⟨y, hy⟩ := not_forall_not.mp hlim
  obtain ⟨i, his, hi⟩ := exists_lt_of_csInf_lt hne hy.lt
  exact eq_of_le_of_not_lt (csInf_le hbdd his) (hy.2 · hi) ▸ his
Infimum is in set when not a predecessor prelimit
Informal description
Let $\alpha$ be a conditionally complete linear order and $s$ a nonempty subset of $\alpha$ that is bounded below. If the infimum $\inf s$ is not a predecessor prelimit (i.e., $\neg\text{IsPredPrelimit}(\inf s)$), then $\inf s$ is an element of $s$.
exists_eq_ciSup_of_not_isSuccPrelimit theorem
(hf : BddAbove (range f)) (hf' : ¬IsSuccPrelimit (⨆ i, f i)) : ∃ i, f i = ⨆ i, f i
Full source 
lemma exists_eq_ciSup_of_not_isSuccPrelimit
    (hf : BddAbove (range f)) (hf' : ¬ IsSuccPrelimit (⨆ i, f i)) : ∃ i, f i = ⨆ i, f i :=
  csSup_mem_of_not_isSuccPrelimit (range_nonempty f) hf hf'
Existence of Attained Supremum for Non-Successor-Prelimit Functions in Conditionally Complete Linear Orders
Informal description
Let $\alpha$ be a conditionally complete linear order and $f : I \to \alpha$ a function with bounded range. If the supremum $\sup_{i} f(i)$ is not a successor prelimit (i.e., $\neg\text{IsSuccPrelimit}(\sup_{i} f(i))$), then there exists an index $i$ such that $f(i) = \sup_{i} f(i)$.
exists_eq_ciInf_of_not_isPredPrelimit theorem
(hf : BddBelow (range f)) (hf' : ¬IsPredPrelimit (⨅ i, f i)) : ∃ i, f i = ⨅ i, f i
Full source 
lemma exists_eq_ciInf_of_not_isPredPrelimit
    (hf : BddBelow (range f)) (hf' : ¬ IsPredPrelimit (⨅ i, f i)) : ∃ i, f i = ⨅ i, f i :=
  csInf_mem_of_not_isPredPrelimit (range_nonempty f) hf hf'
Existence of Attained Infimum for Non-Predecessor-Prelimit Functions in Conditionally Complete Linear Orders
Informal description
Let $\alpha$ be a conditionally complete linear order and $f : I \to \alpha$ a function with bounded below range. If the infimum $\inf_{i} f(i)$ is not a predecessor prelimit (i.e., $\neg\text{IsPredPrelimit}(\inf_{i} f(i))$), then there exists an index $i$ such that $f(i) = \inf_{i} f(i)$.
IsLUB.mem_of_nonempty_of_not_isSuccPrelimit theorem
(hs : IsLUB s x) (hne : s.Nonempty) (hx : ¬IsSuccPrelimit x) : x ∈ s
Full source 
lemma IsLUB.mem_of_nonempty_of_not_isSuccPrelimit
    (hs : IsLUB s x) (hne : s.Nonempty) (hx : ¬ IsSuccPrelimit x) : x ∈ s :=
  hs.csSup_eq hne ▸ csSup_mem_of_not_isSuccPrelimit hne hs.bddAbove (hs.csSup_eq hne ▸ hx)
Membership of Least Upper Bound in Nonempty Set When Not a Successor Prelimit
Informal description
Let $\alpha$ be a conditionally complete linear order, $s$ a nonempty subset of $\alpha$, and $x$ the least upper bound of $s$. If $x$ is not a successor prelimit, then $x$ belongs to $s$.
IsGLB.mem_of_nonempty_of_not_isPredPrelimit theorem
(hs : IsGLB s x) (hne : s.Nonempty) (hx : ¬IsPredPrelimit x) : x ∈ s
Full source 
lemma IsGLB.mem_of_nonempty_of_not_isPredPrelimit
    (hs : IsGLB s x) (hne : s.Nonempty) (hx : ¬ IsPredPrelimit x) : x ∈ s :=
  hs.csInf_eq hne ▸ csInf_mem_of_not_isPredPrelimit hne hs.bddBelow (hs.csInf_eq hne ▸ hx)
Membership of Greatest Lower Bound in Nonempty Set When Not a Predecessor Prelimit
Informal description
Let $\alpha$ be a conditionally complete linear order, $s$ a nonempty subset of $\alpha$, and $x$ the greatest lower bound of $s$. If $x$ is not a predecessor prelimit, then $x$ belongs to $s$.
IsLUB.exists_of_nonempty_of_not_isSuccPrelimit theorem
(hf : IsLUB (range f) x) (hx : ¬IsSuccPrelimit x) : ∃ i, f i = x
Full source 
lemma IsLUB.exists_of_nonempty_of_not_isSuccPrelimit
    (hf : IsLUB (range f) x) (hx : ¬ IsSuccPrelimit x) : ∃ i, f i = x :=
  hf.mem_of_nonempty_of_not_isSuccPrelimit (range_nonempty f) hx
Existence of Attained Supremum for Non-Successor-Prelimit Points in Conditionally Complete Linear Orders
Informal description
Let $\alpha$ be a conditionally complete linear order, $f$ a function with range in $\alpha$, and $x$ the least upper bound of the range of $f$. If $x$ is not a successor prelimit, then there exists an index $i$ such that $f(i) = x$.
IsGLB.exists_of_nonempty_of_not_isPredPrelimit theorem
(hf : IsGLB (range f) x) (hx : ¬IsPredPrelimit x) : ∃ i, f i = x
Full source 
lemma IsGLB.exists_of_nonempty_of_not_isPredPrelimit
    (hf : IsGLB (range f) x) (hx : ¬ IsPredPrelimit x) : ∃ i, f i = x :=
  hf.mem_of_nonempty_of_not_isPredPrelimit (range_nonempty f) hx
Existence of Attained Infimum for Non-Predecessor-Prelimit Points in Conditionally Complete Linear Orders
Informal description
Let $\alpha$ be a conditionally complete linear order, $f$ a function with range in $\alpha$, and $x$ the greatest lower bound of the range of $f$. If $x$ is not a predecessor prelimit, then there exists an index $i$ such that $f(i) = x$.
ConditionallyCompleteLinearOrder.toSuccOrder definition
[WellFoundedLT α] : SuccOrder α
Full source 
/-- Every conditionally complete linear order with well-founded `<` is a successor order, by setting
the successor of an element to be the infimum of all larger elements. -/
noncomputable def ConditionallyCompleteLinearOrder.toSuccOrder [WellFoundedLT α] :
    SuccOrder α where
  succ a := if IsMax a then a else sInf {b | a < b}
  le_succ a := by
    by_cases h : IsMax a
    · simp [h]
    · simp only [h, ↓reduceIte]
      rw [not_isMax_iff] at h
      exact le_csInf h (fun b => le_of_lt)
  max_of_succ_le hs := by
    by_contra h
    simp [h] at hs
    rw [not_isMax_iff] at h
    exact hs.not_lt (csInf_mem h)
  succ_le_of_lt {a b} ha := by
    simp [ha.not_isMax]
    exact csInf_le ⟨a, fun _ hc => hc.le⟩ ha
Successor order structure on a conditionally complete linear order with well-founded $<$
Informal description
Given a conditionally complete linear order $\alpha$ where the relation $<$ is well-founded, we can define a successor order structure on $\alpha$ by setting the successor of an element $a$ to be the infimum of all elements strictly greater than $a$ (if $a$ is not maximal), or $a$ itself (if $a$ is maximal). This construction ensures that $\alpha$ satisfies the properties of a successor order.
csSup_mem_of_not_isSuccPrelimit' theorem
(hbdd : BddAbove s) (hlim : ¬IsSuccPrelimit (sSup s)) : sSup s ∈ s
Full source 
/-- See `csSup_mem_of_not_isSuccPrelimit` for the `ConditionallyCompleteLinearOrder` version. -/
lemma csSup_mem_of_not_isSuccPrelimit'
    (hbdd : BddAbove s) (hlim : ¬ IsSuccPrelimit (sSup s)) : sSupsSup s ∈ s := by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · simp [isSuccPrelimit_bot] at hlim
  · exact csSup_mem_of_not_isSuccPrelimit hs hbdd hlim
Supremum Attainment for Non-Successor-Prelimit Points in Conditionally Complete Linear Orders
Informal description
Let $\alpha$ be a conditionally complete linear order and $s$ a subset of $\alpha$ that is bounded above. If the supremum $\sup s$ is not a successor prelimit, then $\sup s$ is an element of $s$.
exists_eq_ciSup_of_not_isSuccPrelimit' theorem
(hf : BddAbove (range f)) (hf' : ¬IsSuccPrelimit (⨆ i, f i)) : ∃ i, f i = ⨆ i, f i
Full source 
/-- See `exists_eq_ciSup_of_not_isSuccPrelimit` for the
`ConditionallyCompleteLinearOrder` version. -/
lemma exists_eq_ciSup_of_not_isSuccPrelimit'
    (hf : BddAbove (range f)) (hf' : ¬ IsSuccPrelimit (⨆ i, f i)) : ∃ i, f i = ⨆ i, f i :=
  csSup_mem_of_not_isSuccPrelimit' hf hf'
Supremum Attainment for Non-Successor-Prelimit Points in Bounded Functions
Informal description
Let $f$ be a function with values in a conditionally complete linear order with bottom element, and suppose the range of $f$ is bounded above. If the supremum $\bigsqcup_i f(i)$ is not a successor prelimit point, then there exists an index $i$ such that $f(i) = \bigsqcup_i f(i)$.
IsLUB.exists_of_not_isSuccPrelimit theorem
(hf : IsLUB (range f) x) (hx : ¬IsSuccPrelimit x) : ∃ i, f i = x
Full source 
@[deprecated IsLUB.mem_of_not_isSuccPrelimit (since := "2025-01-05")]
lemma IsLUB.exists_of_not_isSuccPrelimit (hf : IsLUB (range f) x) (hx : ¬ IsSuccPrelimit x) :
    ∃ i, f i = x :=
  hf.mem_of_not_isSuccPrelimit hx
Existence of Attained Supremum for Non-Successor-Prelimit Points
Informal description
Let $f$ be a function with values in a conditionally complete linear order, and let $x$ be the least upper bound of the range of $f$. If $x$ is not a successor pre-limit point, then there exists an index $i$ such that $f(i) = x$.
Order.IsSuccPrelimit.sSup_Iio theorem
(h : IsSuccPrelimit x) : sSup (Iio x) = x
Full source 
theorem Order.IsSuccPrelimit.sSup_Iio (h : IsSuccPrelimit x) : sSup (Iio x) = x := by
  obtain rfl | hx := eq_bot_or_bot_lt x
  · simp
  · exact h.isLUB_Iio.csSup_eq ⟨⊥, hx⟩
Supremum of Strictly Below Elements Equals Successor Prelimit Point
Informal description
Let $\alpha$ be a conditionally complete linear order with a bottom element, and let $x \in \alpha$ be a successor pre-limit point. Then the supremum of the left-infinite right-open interval $(-\infty, x)$ is equal to $x$, i.e., $\sup \{a \in \alpha \mid a < x\} = x$.
Order.IsSuccPrelimit.iSup_Iio theorem
(h : IsSuccPrelimit x) : ⨆ a : Iio x, a.1 = x
Full source 
theorem Order.IsSuccPrelimit.iSup_Iio (h : IsSuccPrelimit x) : ⨆ a : Iio x, a.1 = x := by
  rw [← sSup_eq_iSup', h.sSup_Iio]
Supremum of Strictly Below Elements Equals Successor Prelimit Point
Informal description
Let $\alpha$ be a conditionally complete linear order with a bottom element, and let $x \in \alpha$ be a successor pre-limit point. Then the supremum of the elements in the interval $(-\infty, x)$ is equal to $x$, i.e., $\sup \{a \in \alpha \mid a < x\} = x$.
Order.IsSuccLimit.sSup_Iio theorem
(h : IsSuccLimit x) : sSup (Iio x) = x
Full source 
theorem Order.IsSuccLimit.sSup_Iio (h : IsSuccLimit x) : sSup (Iio x) = x :=
  h.isSuccPrelimit.sSup_Iio
Supremum of Strictly Below Elements Equals Successor Limit Point
Informal description
Let $\alpha$ be a conditionally complete linear order with a bottom element, and let $x \in \alpha$ be a successor limit point. Then the supremum of the left-infinite right-open interval $(-\infty, x)$ is equal to $x$, i.e., $\sup \{a \in \alpha \mid a < x\} = x$.
Order.IsSuccLimit.iSup_Iio theorem
(h : IsSuccLimit x) : ⨆ a : Iio x, a.1 = x
Full source 
theorem Order.IsSuccLimit.iSup_Iio (h : IsSuccLimit x) : ⨆ a : Iio x, a.1 = x :=
  h.isSuccPrelimit.iSup_Iio
Supremum of Strictly Below Elements Equals Successor Limit Point
Informal description
Let $\alpha$ be a conditionally complete linear order with a bottom element, and let $x \in \alpha$ be a successor limit point. Then the supremum of the elements strictly below $x$ is equal to $x$, i.e., \[ \sup \{a \in \alpha \mid a < x\} = x. \]
sSup_Iio_eq_self_iff_isSuccPrelimit theorem
: sSup (Iio x) = x ↔ IsSuccPrelimit x
Full source 
theorem sSup_Iio_eq_self_iff_isSuccPrelimit : sSupsSup (Iio x) = x ↔ IsSuccPrelimit x := by
  refine ⟨fun h ↦ ?_, IsSuccPrelimit.sSup_Iio⟩
  by_contra hx
  rw [← h] at hx
  simpa [h] using csSup_mem_of_not_isSuccPrelimit' bddAbove_Iio hx
Characterization of Successor Prelimit Points via Supremum of Strictly Below Elements
Informal description
Let $\alpha$ be a conditionally complete linear order with a bottom element, and let $x \in \alpha$. The supremum of the left-infinite right-open interval $(-\infty, x)$ equals $x$ if and only if $x$ is a successor prelimit point. In symbols: \[ \sup \{a \in \alpha \mid a < x\} = x \leftrightarrow \text{IsSuccPrelimit}(x). \]
iSup_Iio_eq_self_iff_isSuccPrelimit theorem
: ⨆ a : Iio x, a.1 = x ↔ IsSuccPrelimit x
Full source 
theorem iSup_Iio_eq_self_iff_isSuccPrelimit : ⨆ a : Iio x, a.1⨆ a : Iio x, a.1 = x ↔ IsSuccPrelimit x := by
  rw [← sSup_eq_iSup', sSup_Iio_eq_self_iff_isSuccPrelimit]
Characterization of Successor Prelimit Points via Supremum of Strictly Below Elements
Informal description
Let $\alpha$ be a conditionally complete linear order with a bottom element, and let $x \in \alpha$. The supremum of the set $\{a \in \alpha \mid a < x\}$ equals $x$ if and only if $x$ is a successor prelimit point. In symbols: \[ \sup \{a \in \alpha \mid a < x\} = x \leftrightarrow \text{IsSuccPrelimit}(x). \]
iSup_succ theorem
[SuccOrder α] (x : α) : ⨆ a : Iio x, succ a.1 = x
Full source 
theorem iSup_succ [SuccOrder α] (x : α) : ⨆ a : Iio x, succ a.1 = x := by
  have H : BddAbove (range fun a : Iio x ↦ succ a.1) :=
    ⟨succ x, by simp +contextual [upperBounds, succ_le_succ, le_of_lt]⟩
  apply le_antisymm _ (le_of_forall_lt fun y hy ↦ ?_)
  · rw [ciSup_le_iff' H]
    exact fun a ↦ succ_le_of_lt a.2
  · rw [lt_ciSup_iff' H]
    exact ⟨⟨y, hy⟩, lt_succ_of_not_isMax hy.not_isMax⟩
Supremum of Successors in Left-Infinite Interval Equals Element
Informal description
Let $\alpha$ be a conditionally complete linear order with a successor function. For any element $x \in \alpha$, the supremum of the successors of all elements less than $x$ is equal to $x$. In symbols: \[ \bigsqcup_{a < x} \text{succ}(a) = x. \]
sSup_mem_of_not_isSuccPrelimit theorem
(hlim : ¬IsSuccPrelimit (sSup s)) : sSup s ∈ s
Full source 
lemma sSup_mem_of_not_isSuccPrelimit (hlim : ¬ IsSuccPrelimit (sSup s)) : sSupsSup s ∈ s := by
  obtain ⟨y, hy⟩ := not_forall_not.mp hlim
  obtain ⟨i, his, hi⟩ := lt_sSup_iff.mp hy.lt
  exact eq_of_le_of_not_lt (le_sSup his) (hy.2 hi) ▸ his
Membership of Supremum in Set When Not a Successor Pre-limit Point
Informal description
For any subset $s$ of a conditionally complete linear order, if the supremum $\sup s$ is not a successor pre-limit point, then $\sup s$ belongs to $s$.
sInf_mem_of_not_isPredPrelimit theorem
(hlim : ¬IsPredPrelimit (sInf s)) : sInf s ∈ s
Full source 
lemma sInf_mem_of_not_isPredPrelimit (hlim : ¬ IsPredPrelimit (sInf s)) : sInfsInf s ∈ s := by
  obtain ⟨y, hy⟩ := not_forall_not.mp hlim
  obtain ⟨i, his, hi⟩ := sInf_lt_iff.mp hy.lt
  exact eq_of_le_of_not_lt (sInf_le his) (hy.2 · hi) ▸ his
Membership of Infimum in Set When Not a Predecessor Pre-limit Point
Informal description
For a set $s$ in a conditionally complete linear order, if the infimum $\inf s$ is not a predecessor pre-limit point, then $\inf s$ is an element of $s$.
exists_eq_iSup_of_not_isSuccPrelimit theorem
(hf : ¬IsSuccPrelimit (⨆ i, f i)) : ∃ i, f i = ⨆ i, f i
Full source 
lemma exists_eq_iSup_of_not_isSuccPrelimit (hf : ¬ IsSuccPrelimit (⨆ i, f i)) :
    ∃ i, f i = ⨆ i, f i :=
  sSup_mem_of_not_isSuccPrelimit hf
Existence of Attaining Index for Supremum When Not a Successor Pre-limit Point
Informal description
For a family of elements $(f_i)_{i \in I}$ in a conditionally complete linear order, if the supremum $\bigsqcup_i f_i$ is not a successor pre-limit point, then there exists an index $i$ such that $f_i = \bigsqcup_i f_i$.
exists_eq_iInf_of_not_isPredPrelimit theorem
(hf : ¬IsPredPrelimit (⨅ i, f i)) : ∃ i, f i = ⨅ i, f i
Full source 
lemma exists_eq_iInf_of_not_isPredPrelimit (hf : ¬ IsPredPrelimit (⨅ i, f i)) :
    ∃ i, f i = ⨅ i, f i :=
  sInf_mem_of_not_isPredPrelimit hf
Existence of Attained Infimum When Not a Predecessor Pre-limit Point
Informal description
For a family of elements $(f_i)_{i \in I}$ in a conditionally complete linear order, if the infimum $\inf_i f_i$ is not a predecessor pre-limit point, then there exists an index $i$ such that $f_i = \inf_i f_i$.
IsGLB.exists_of_not_isPredPrelimit theorem
(hf : IsGLB (range f) x) (hx : ¬IsPredPrelimit x) : ∃ i, f i = x
Full source 
@[deprecated IsGLB.mem_of_not_isPredLimit (since := "2025-01-05")]
lemma IsGLB.exists_of_not_isPredPrelimit (hf : IsGLB (range f) x) (hx : ¬ IsPredPrelimit x) :
    ∃ i, f i = x :=
  hf.mem_of_not_isPredPrelimit hx
Attainment of Greatest Lower Bound When Not a Predecessor Pre-limit Point
Informal description
Let $(f_i)_{i \in I}$ be a family of elements in a conditionally complete linear order, and let $x$ be the greatest lower bound of the range of $f$. If $x$ is not a predecessor pre-limit point, then there exists an index $i$ such that $f_i = x$.