Mathlib.Order.Bounds.Basic

mem_upperBounds theorem

: a ∈ upperBounds s ↔ ∀ x ∈ s, x ≤ a

Full source

theorem mem_upperBounds : a ∈ upperBounds sa ∈ upperBounds s ↔ ∀ x ∈ s, x ≤ a :=
  Iff.rfl

Characterization of Upper Bounds: $a \in \text{upperBounds}(s) \leftrightarrow \forall x \in s, x \leq a$

Informal description

An element $a$ belongs to the set of upper bounds of a set $s$ if and only if for every element $x \in s$, we have $x \leq a$.

mem_lowerBounds theorem

: a ∈ lowerBounds s ↔ ∀ x ∈ s, a ≤ x

Full source

theorem mem_lowerBounds : a ∈ lowerBounds sa ∈ lowerBounds s ↔ ∀ x ∈ s, a ≤ x :=
  Iff.rfl

Characterization of Lower Bounds: $a \in \text{lowerBounds}(s) \leftrightarrow \forall x \in s, a \leq x$

Informal description

An element $a$ belongs to the set of lower bounds of a set $s$ in a partially ordered type if and only if $a$ is less than or equal to every element $x$ in $s$, i.e., $a \in \text{lowerBounds}(s) \leftrightarrow \forall x \in s, a \leq x$.

mem_upperBounds_iff_subset_Iic theorem

: a ∈ upperBounds s ↔ s ⊆ Iic a

Full source

lemma mem_upperBounds_iff_subset_Iic : a ∈ upperBounds sa ∈ upperBounds s ↔ s ⊆ Iic a := Iff.rfl

Characterization of Upper Bounds via Interval Inclusion

Informal description

An element $a$ is an upper bound of a set $s$ in a preorder if and only if $s$ is a subset of the left-infinite right-closed interval $(-\infty, a]$.

mem_lowerBounds_iff_subset_Ici theorem

: a ∈ lowerBounds s ↔ s ⊆ Ici a

Full source

lemma mem_lowerBounds_iff_subset_Ici : a ∈ lowerBounds sa ∈ lowerBounds s ↔ s ⊆ Ici a := Iff.rfl

Characterization of Lower Bounds via Interval Containment

Informal description

An element $a$ in a preorder $\alpha$ is a lower bound of a set $s \subseteq \alpha$ if and only if $s$ is contained in the right-infinite interval $[a, \infty)$, i.e., $s \subseteq \{x \in \alpha \mid a \leq x\}$.

bddAbove_def theorem

: BddAbove s ↔ ∃ x, ∀ y ∈ s, y ≤ x

Full source

theorem bddAbove_def : BddAboveBddAbove s ↔ ∃ x, ∀ y ∈ s, y ≤ x :=
  Iff.rfl

Characterization of Bounded Above Sets via Upper Bounds

Informal description

A set $s$ in a preorder is bounded above if and only if there exists an element $x$ such that $y \leq x$ for all $y \in s$.

bddBelow_def theorem

: BddBelow s ↔ ∃ x, ∀ y ∈ s, x ≤ y

Full source

theorem bddBelow_def : BddBelowBddBelow s ↔ ∃ x, ∀ y ∈ s, x ≤ y :=
  Iff.rfl

Characterization of Bounded Below Sets via Lower Bounds

Informal description

A set $s$ in a preorder is bounded below if and only if there exists an element $x$ such that $x \leq y$ for all $y \in s$.

bot_mem_lowerBounds theorem

[OrderBot α] (s : Set α) : ⊥ ∈ lowerBounds s

Full source

theorem bot_mem_lowerBounds [OrderBot α] (s : Set α) : ⊥⊥ ∈ lowerBounds s := fun _ _ => bot_le

Bottom Element is a Lower Bound for Any Set

Informal description

In an order with a bottom element $\bot$, the bottom element is a lower bound for any set $s$, i.e., $\bot \in \text{lowerBounds}(s)$.

top_mem_upperBounds theorem

[OrderTop α] (s : Set α) : ⊤ ∈ upperBounds s

Full source

theorem top_mem_upperBounds [OrderTop α] (s : Set α) : ⊤⊤ ∈ upperBounds s := fun _ _ => le_top

Top Element is an Upper Bound for Any Set

Informal description

In an ordered set $\alpha$ with a greatest element $\top$, the top element is an upper bound for any subset $s \subseteq \alpha$, i.e., $\top \in \text{upperBounds}(s)$.

isLeast_bot_iff theorem

[OrderBot α] : IsLeast s ⊥ ↔ ⊥ ∈ s

Full source

@[simp]
theorem isLeast_bot_iff [OrderBot α] : IsLeastIsLeast s ⊥ ↔ ⊥ ∈ s :=
  and_iff_left <| bot_mem_lowerBounds _

Characterization of Least Element as Bottom Element in Ordered Sets

Informal description

In an order with a bottom element $\bot$, the element $\bot$ is the least element of a set $s$ if and only if $\bot$ belongs to $s$.

isGreatest_top_iff theorem

[OrderTop α] : IsGreatest s ⊤ ↔ ⊤ ∈ s

Full source

@[simp]
theorem isGreatest_top_iff [OrderTop α] : IsGreatestIsGreatest s ⊤ ↔ ⊤ ∈ s :=
  and_iff_left <| top_mem_upperBounds _

Characterization of Greatest Element as Top Element: $\text{IsGreatest}(s, \top) \leftrightarrow \top \in s$

Informal description

In an ordered set $\alpha$ with a greatest element $\top$, the element $\top$ is the greatest element of a subset $s \subseteq \alpha$ if and only if $\top$ belongs to $s$.

not_bddAbove_iff' theorem

: ¬BddAbove s ↔ ∀ x, ∃ y ∈ s, ¬y ≤ x

Full source

/-- A set `s` is not bounded above if and only if for each `x` there exists `y ∈ s` such that `x`
is not greater than or equal to `y`. This version only assumes `Preorder` structure and uses
`¬(y ≤ x)`. A version for linear orders is called `not_bddAbove_iff`. -/
theorem not_bddAbove_iff' : ¬BddAbove s¬BddAbove s ↔ ∀ x, ∃ y ∈ s, ¬y ≤ x := by
  simp [BddAbove, upperBounds, Set.Nonempty]

Characterization of Unbounded Above Sets in Preorders

Informal description

A set $s$ in a preorder is not bounded above if and only if for every element $x$, there exists an element $y \in s$ such that $y \not\leq x$.

not_bddBelow_iff' theorem

: ¬BddBelow s ↔ ∀ x, ∃ y ∈ s, ¬x ≤ y

Full source

/-- A set `s` is not bounded below if and only if for each `x` there exists `y ∈ s` such that `x`
is not less than or equal to `y`. This version only assumes `Preorder` structure and uses
`¬(x ≤ y)`. A version for linear orders is called `not_bddBelow_iff`. -/
theorem not_bddBelow_iff' : ¬BddBelow s¬BddBelow s ↔ ∀ x, ∃ y ∈ s, ¬x ≤ y :=
  @not_bddAbove_iff' αᵒᵈ _ _

Characterization of Unbounded Below Sets in Preorders: $\neg\text{BddBelow}(s) \leftrightarrow \forall x, \exists y \in s, \neg(x \leq y)$

Informal description

A set $s$ in a preorder is not bounded below if and only if for every element $x$, there exists an element $y \in s$ such that $x \not\leq y$.

not_bddAbove_iff theorem

{α : Type*} [LinearOrder α] {s : Set α} : ¬BddAbove s ↔ ∀ x, ∃ y ∈ s, x < y

Full source

/-- A set `s` is not bounded above if and only if for each `x` there exists `y ∈ s` that is greater
than `x`. A version for preorders is called `not_bddAbove_iff'`. -/
theorem not_bddAbove_iff {α : Type*} [LinearOrder α] {s : Set α} :
    ¬BddAbove s¬BddAbove s ↔ ∀ x, ∃ y ∈ s, x < y := by
  simp only [not_bddAbove_iff', not_le]

Characterization of Unbounded Above Sets in Linear Orders: $\neg\text{BddAbove}(s) \leftrightarrow \forall x, \exists y \in s, x < y$

Informal description

For a set $s$ in a linearly ordered type $\alpha$, $s$ is not bounded above if and only if for every element $x \in \alpha$, there exists an element $y \in s$ such that $x < y$.

not_bddBelow_iff theorem

{α : Type*} [LinearOrder α] {s : Set α} : ¬BddBelow s ↔ ∀ x, ∃ y ∈ s, y < x

Full source

/-- A set `s` is not bounded below if and only if for each `x` there exists `y ∈ s` that is less
than `x`. A version for preorders is called `not_bddBelow_iff'`. -/
theorem not_bddBelow_iff {α : Type*} [LinearOrder α] {s : Set α} :
    ¬BddBelow s¬BddBelow s ↔ ∀ x, ∃ y ∈ s, y < x :=
  @not_bddAbove_iff αᵒᵈ _ _

Characterization of Unbounded Below Sets in Linear Orders: $\neg\text{BddBelow}(s) \leftrightarrow \forall x, \exists y \in s, y < x$

Informal description

For a set $s$ in a linearly ordered type $\alpha$, $s$ is not bounded below if and only if for every element $x \in \alpha$, there exists an element $y \in s$ such that $y < x$.

bddBelow_preimage_ofDual theorem

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

Full source

@[simp] lemma bddBelow_preimage_ofDual {s : Set α} : BddBelowBddBelow (ofDual ⁻¹' s) ↔ BddAbove s := Iff.rfl

Bounded Below Preimage of Order-Reversed Set is Equivalent to Bounded Above Original Set

Informal description

For any set $s$ in a type $\alpha$ with a preorder, the preimage of $s$ under the order-reversing map `ofDual` is bounded below if and only if $s$ itself is bounded above.

bddAbove_preimage_ofDual theorem

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

Full source

@[simp] lemma bddAbove_preimage_ofDual {s : Set α} : BddAboveBddAbove (ofDual ⁻¹' s) ↔ BddBelow s := Iff.rfl

Bounded Above Preimage of Order-Reversed Set is Equivalent to Bounded Below Original Set

Informal description

For any set $s$ in a type $\alpha$ with a preorder, the preimage of $s$ under the order-reversing map `ofDual` is bounded above if and only if $s$ itself is bounded below.

bddBelow_preimage_toDual theorem

{s : Set αᵒᵈ} : BddBelow (toDual ⁻¹' s) ↔ BddAbove s

Full source

@[simp] lemma bddBelow_preimage_toDual {s : Set αᵒᵈ} :
    BddBelowBddBelow (toDual ⁻¹' s) ↔ BddAbove s := Iff.rfl

Bounded Below Preimage under Order-Reversal is Equivalent to Bounded Above Original Set

Informal description

For any set $s$ in the order-dual type $\alpha^\mathrm{op}$, the preimage of $s$ under the order-reversing map `toDual` is bounded below if and only if $s$ is bounded above in $\alpha^\mathrm{op}$.

bddAbove_preimage_toDual theorem

{s : Set αᵒᵈ} : BddAbove (toDual ⁻¹' s) ↔ BddBelow s

Full source

@[simp] lemma bddAbove_preimage_toDual {s : Set αᵒᵈ} :
    BddAboveBddAbove (toDual ⁻¹' s) ↔ BddBelow s := Iff.rfl

Bounded Above Preimage under Order-Reversal is Equivalent to Bounded Below Original Set

Informal description

For any set $s$ in the order-dual type $\alpha^\mathrm{op}$, the preimage of $s$ under the order-reversing map `toDual` is bounded above if and only if $s$ is bounded below in $\alpha^\mathrm{op}$.

BddAbove.dual theorem

(h : BddAbove s) : BddBelow (ofDual ⁻¹' s)

Full source

theorem BddAbove.dual (h : BddAbove s) : BddBelow (ofDualofDual ⁻¹' s) :=
  h

Order Duality of Bounded Above Sets

Informal description

If a set $s$ in a partially ordered type $\alpha$ is bounded above, then the preimage of $s$ under the order-reversing map `ofDual` is bounded below in the order-dual type $\alpha^\mathrm{op}$.

BddBelow.dual theorem

(h : BddBelow s) : BddAbove (ofDual ⁻¹' s)

Full source

theorem BddBelow.dual (h : BddBelow s) : BddAbove (ofDualofDual ⁻¹' s) :=
  h

Order Duality of Bounded Below Sets

Informal description

If a set $s$ in a partially ordered type $\alpha$ is bounded below, then the preimage of $s$ under the order-reversing map `ofDual` is bounded above in the order-dual type $\alpha^\mathrm{op}$.

IsLeast.dual theorem

(h : IsLeast s a) : IsGreatest (ofDual ⁻¹' s) (toDual a)

Full source

theorem IsLeast.dual (h : IsLeast s a) : IsGreatest (ofDualofDual ⁻¹' s) (toDual a) :=
  h

Dual of Least Element is Greatest Element in Order-Reversed Set

Informal description

If an element $a$ is the least element of a set $s$ in a partially ordered type $\alpha$, then its dual (under the order-reversing equivalence) is the greatest element of the preimage of $s$ under the order-reversing map.

IsGreatest.dual theorem

(h : IsGreatest s a) : IsLeast (ofDual ⁻¹' s) (toDual a)

Full source

theorem IsGreatest.dual (h : IsGreatest s a) : IsLeast (ofDualofDual ⁻¹' s) (toDual a) :=
  h

Dual of Greatest Element is Least Element in Order-Reversed Set

Informal description

If an element $a$ is the greatest element of a set $s$ in a partially ordered type $\alpha$, then its dual (under the order-reversing equivalence) is the least element of the preimage of $s$ under the order-reversing map.

IsLUB.dual theorem

(h : IsLUB s a) : IsGLB (ofDual ⁻¹' s) (toDual a)

Full source

theorem IsLUB.dual (h : IsLUB s a) : IsGLB (ofDualofDual ⁻¹' s) (toDual a) :=
  h

Dual of Least Upper Bound is Greatest Lower Bound in Order-Reversed Set

Informal description

Let $s$ be a subset of a partially ordered type $\alpha$ and let $a \in \alpha$ be the least upper bound (supremum) of $s$. Then, under the order-reversing equivalence, the dual of $a$ is the greatest lower bound (infimum) of the preimage of $s$ under the order-reversing map.

IsGLB.dual theorem

(h : IsGLB s a) : IsLUB (ofDual ⁻¹' s) (toDual a)

Full source

theorem IsGLB.dual (h : IsGLB s a) : IsLUB (ofDualofDual ⁻¹' s) (toDual a) :=
  h

Dual of Greatest Lower Bound is Least Upper Bound in Order-Reversed Set

Informal description

If an element $a$ is the greatest lower bound (infimum) of a set $s$ in a partially ordered type $\alpha$, then its dual (under the order-reversing equivalence) is the least upper bound (supremum) of the preimage of $s$ under the order-reversing map.

IsLeast.orderBot abbrev

(h : IsLeast s a) : OrderBot s

Full source

/-- If `a` is the least element of a set `s`, then subtype `s` is an order with bottom element. -/
abbrev IsLeast.orderBot (h : IsLeast s a) :
    OrderBot s where
  bot := ⟨a, h.1⟩
  bot_le := Subtype.forall.2 h.2

Subtype Order with Bottom Element from Least Element

Informal description

If $a$ is the least element of a set $s$ in a partially ordered type $\alpha$, then the subtype $s$ can be equipped with the structure of an order with a bottom element, where $a$ serves as the least element $\bot$.

IsGreatest.orderTop abbrev

(h : IsGreatest s a) : OrderTop s

Full source

/-- If `a` is the greatest element of a set `s`, then subtype `s` is an order with top element. -/
abbrev IsGreatest.orderTop (h : IsGreatest s a) :
    OrderTop s where
  top := ⟨a, h.1⟩
  le_top := Subtype.forall.2 h.2

Subtype Order with Top Element from Greatest Element

Informal description

If an element $a$ is the greatest element of a set $s$ in a partially ordered type $\alpha$, then the subtype $s$ can be equipped with the structure of an order with a top element, where $a$ serves as the greatest element $\top$.

isLUB_congr theorem

(h : upperBounds s = upperBounds t) : IsLUB s a ↔ IsLUB t a

Full source

theorem isLUB_congr (h : upperBounds s = upperBounds t) : IsLUBIsLUB s a ↔ IsLUB t a := by
  rw [IsLUB, IsLUB, h]

Least Upper Bound Characterization via Equal Upper Bounds

Informal description

For any two sets $s$ and $t$ in a preordered type $\alpha$, if the sets of upper bounds of $s$ and $t$ are equal, then an element $a \in \alpha$ is the least upper bound of $s$ if and only if it is the least upper bound of $t$.

isGLB_congr theorem

(h : lowerBounds s = lowerBounds t) : IsGLB s a ↔ IsGLB t a

Full source

theorem isGLB_congr (h : lowerBounds s = lowerBounds t) : IsGLBIsGLB s a ↔ IsGLB t a := by
  rw [IsGLB, IsGLB, h]

Greatest Lower Bound Characterization via Equal Lower Bounds

Informal description

For any two sets $s$ and $t$ in a partially ordered type $\alpha$, if the sets of lower bounds of $s$ and $t$ are equal, then an element $a \in \alpha$ is the greatest lower bound of $s$ if and only if it is the greatest lower bound of $t$.

upperBounds_mono_set theorem

⦃s t : Set α⦄ (hst : s ⊆ t) : upperBounds t ⊆ upperBounds s

Full source

theorem upperBounds_mono_set ⦃s t : Set α⦄ (hst : s ⊆ t) : upperBoundsupperBounds t ⊆ upperBounds s :=
  fun _ hb _ h => hb <| hst h

Monotonicity of Upper Bounds with Respect to Set Inclusion

Informal description

For any two sets $s$ and $t$ in a preordered type $\alpha$, if $s$ is a subset of $t$, then the set of upper bounds of $t$ is a subset of the set of upper bounds of $s$.

lowerBounds_mono_set theorem

⦃s t : Set α⦄ (hst : s ⊆ t) : lowerBounds t ⊆ lowerBounds s

Full source

theorem lowerBounds_mono_set ⦃s t : Set α⦄ (hst : s ⊆ t) : lowerBoundslowerBounds t ⊆ lowerBounds s :=
  fun _ hb _ h => hb <| hst h

Monotonicity of Lower Bounds under Subset Inclusion

Informal description

For any sets $s$ and $t$ in a partially ordered type $\alpha$, if $s$ is a subset of $t$, then the set of lower bounds of $t$ is a subset of the set of lower bounds of $s$.

upperBounds_mono_mem theorem

⦃a b⦄ (hab : a ≤ b) : a ∈ upperBounds s → b ∈ upperBounds s

Full source

theorem upperBounds_mono_mem ⦃a b⦄ (hab : a ≤ b) : a ∈ upperBounds s → b ∈ upperBounds s :=
  fun ha _ h => le_trans (ha h) hab

Monotonicity of Upper Bounds with Respect to Order

Informal description

For any elements $a$ and $b$ in a preordered type $\alpha$, if $a \leq b$ and $a$ is an upper bound of a set $s \subseteq \alpha$, then $b$ is also an upper bound of $s$.

lowerBounds_mono_mem theorem

⦃a b⦄ (hab : a ≤ b) : b ∈ lowerBounds s → a ∈ lowerBounds s

Full source

theorem lowerBounds_mono_mem ⦃a b⦄ (hab : a ≤ b) : b ∈ lowerBounds s → a ∈ lowerBounds s :=
  fun hb _ h => le_trans hab (hb h)

Monotonicity of Lower Bounds with Respect to Order

Informal description

For any elements $a$ and $b$ in a partially ordered type $\alpha$, if $a \leq b$ and $b$ is a lower bound of a set $s \subseteq \alpha$, then $a$ is also a lower bound of $s$.

upperBounds_mono theorem

⦃s t : Set α⦄ (hst : s ⊆ t) ⦃a b⦄ (hab : a ≤ b) : a ∈ upperBounds t → b ∈ upperBounds s

Full source

theorem upperBounds_mono ⦃s t : Set α⦄ (hst : s ⊆ t) ⦃a b⦄ (hab : a ≤ b) :
    a ∈ upperBounds t → b ∈ upperBounds s := fun ha =>
  upperBounds_mono_set hst <| upperBounds_mono_mem hab ha

Monotonicity of Upper Bounds under Subset and Order Relation

Informal description

For any sets $s$ and $t$ in a preordered type $\alpha$, if $s \subseteq t$ and for any elements $a, b \in \alpha$ with $a \leq b$, then whenever $a$ is an upper bound of $t$, it follows that $b$ is an upper bound of $s$.

lowerBounds_mono theorem

⦃s t : Set α⦄ (hst : s ⊆ t) ⦃a b⦄ (hab : a ≤ b) : b ∈ lowerBounds t → a ∈ lowerBounds s

Full source

theorem lowerBounds_mono ⦃s t : Set α⦄ (hst : s ⊆ t) ⦃a b⦄ (hab : a ≤ b) :
    b ∈ lowerBounds t → a ∈ lowerBounds s := fun hb =>
  lowerBounds_mono_set hst <| lowerBounds_mono_mem hab hb

Monotonicity of Lower Bounds under Subset and Order Relation

Informal description

For any sets $s$ and $t$ in a partially ordered type $\alpha$, if $s \subseteq t$ and for any elements $a, b \in \alpha$ with $a \leq b$, then whenever $b$ is a lower bound of $t$, it follows that $a$ is a lower bound of $s$.

BddAbove.mono theorem

⦃s t : Set α⦄ (h : s ⊆ t) : BddAbove t → BddAbove s

Full source

/-- If `s ⊆ t` and `t` is bounded above, then so is `s`. -/
theorem BddAbove.mono ⦃s t : Set α⦄ (h : s ⊆ t) : BddAbove t → BddAbove s :=
  Nonempty.mono <| upperBounds_mono_set h

Subset of Bounded Above Set is Bounded Above

Informal description

For any sets $s$ and $t$ in a preordered type $\alpha$, if $s \subseteq t$ and $t$ is bounded above, then $s$ is also bounded above.

BddBelow.mono theorem

⦃s t : Set α⦄ (h : s ⊆ t) : BddBelow t → BddBelow s

Full source

/-- If `s ⊆ t` and `t` is bounded below, then so is `s`. -/
theorem BddBelow.mono ⦃s t : Set α⦄ (h : s ⊆ t) : BddBelow t → BddBelow s :=
  Nonempty.mono <| lowerBounds_mono_set h

Subset of Bounded Below Set is Bounded Below

Informal description

For any sets $s$ and $t$ in a partially ordered type $\alpha$, if $s$ is a subset of $t$ and $t$ is bounded below, then $s$ is also bounded below.

IsLUB.of_subset_of_superset theorem

{s t p : Set α} (hs : IsLUB s a) (hp : IsLUB p a) (hst : s ⊆ t) (htp : t ⊆ p) : IsLUB t a

Full source

/-- If `a` is a least upper bound for sets `s` and `p`, then it is a least upper bound for any
set `t`, `s ⊆ t ⊆ p`. -/
theorem IsLUB.of_subset_of_superset {s t p : Set α} (hs : IsLUB s a) (hp : IsLUB p a) (hst : s ⊆ t)
    (htp : t ⊆ p) : IsLUB t a :=
  ⟨upperBounds_mono_set htp hp.1, lowerBounds_mono_set (upperBounds_mono_set hst) hs.2⟩

Supremum Preservation under Intermediate Set Inclusion

Informal description

Let $s$, $t$, and $p$ be subsets of a partially ordered set $\alpha$, with $s \subseteq t \subseteq p$. If $a$ is a least upper bound (supremum) for both $s$ and $p$, then $a$ is also a least upper bound for $t$.

IsGLB.of_subset_of_superset theorem

{s t p : Set α} (hs : IsGLB s a) (hp : IsGLB p a) (hst : s ⊆ t) (htp : t ⊆ p) : IsGLB t a

Full source

/-- If `a` is a greatest lower bound for sets `s` and `p`, then it is a greater lower bound for any
set `t`, `s ⊆ t ⊆ p`. -/
theorem IsGLB.of_subset_of_superset {s t p : Set α} (hs : IsGLB s a) (hp : IsGLB p a) (hst : s ⊆ t)
    (htp : t ⊆ p) : IsGLB t a :=
  hs.dual.of_subset_of_superset hp hst htp

Infimum Preservation under Intermediate Set Inclusion

Informal description

Let $s$, $t$, and $p$ be subsets of a partially ordered set $\alpha$ such that $s \subseteq t \subseteq p$. If $a$ is a greatest lower bound (infimum) for both $s$ and $p$, then $a$ is also a greatest lower bound for $t$.

IsLeast.mono theorem

(ha : IsLeast s a) (hb : IsLeast t b) (hst : s ⊆ t) : b ≤ a

Full source

theorem IsLeast.mono (ha : IsLeast s a) (hb : IsLeast t b) (hst : s ⊆ t) : b ≤ a :=
  hb.2 (hst ha.1)

Monotonicity of Least Elements under Set Inclusion

Informal description

Let $s$ and $t$ be sets in a partially ordered type $\alpha$, with $s \subseteq t$. If $a$ is the least element of $s$ and $b$ is the least element of $t$, then $b \leq a$.

IsGreatest.mono theorem

(ha : IsGreatest s a) (hb : IsGreatest t b) (hst : s ⊆ t) : a ≤ b

Full source

theorem IsGreatest.mono (ha : IsGreatest s a) (hb : IsGreatest t b) (hst : s ⊆ t) : a ≤ b :=
  hb.2 (hst ha.1)

Monotonicity of Greatest Elements under Set Inclusion

Informal description

Let $s$ and $t$ be sets in a partially ordered type $\alpha$, with $s \subseteq t$. If $a$ is the greatest element of $s$ and $b$ is the greatest element of $t$, then $a \leq b$.

IsLUB.mono theorem

(ha : IsLUB s a) (hb : IsLUB t b) (hst : s ⊆ t) : a ≤ b

Full source

theorem IsLUB.mono (ha : IsLUB s a) (hb : IsLUB t b) (hst : s ⊆ t) : a ≤ b :=
  IsLeast.mono hb ha <| upperBounds_mono_set hst

Monotonicity of Least Upper Bounds under Set Inclusion

Informal description

Let $s$ and $t$ be subsets of a partially ordered set $\alpha$ with $s \subseteq t$. If $a$ is the least upper bound of $s$ and $b$ is the least upper bound of $t$, then $a \leq b$.

IsGLB.mono theorem

(ha : IsGLB s a) (hb : IsGLB t b) (hst : s ⊆ t) : b ≤ a

Full source

theorem IsGLB.mono (ha : IsGLB s a) (hb : IsGLB t b) (hst : s ⊆ t) : b ≤ a :=
  IsGreatest.mono hb ha <| lowerBounds_mono_set hst

Monotonicity of Greatest Lower Bounds under Set Inclusion

Informal description

Let $s$ and $t$ be subsets of a partially ordered set $\alpha$ with $s \subseteq t$. If $a$ is the greatest lower bound of $s$ and $b$ is the greatest lower bound of $t$, then $b \leq a$.

subset_lowerBounds_upperBounds theorem

(s : Set α) : s ⊆ lowerBounds (upperBounds s)

Full source

theorem subset_lowerBounds_upperBounds (s : Set α) : s ⊆ lowerBounds (upperBounds s) :=
  fun _ hx _ hy => hy hx

Elements are lower bounds of their upper bounds

Informal description

For any subset $s$ of a partially ordered set $\alpha$, every element of $s$ is a lower bound of the set of upper bounds of $s$. In other words, if $x \in s$ and $y$ is an upper bound of $s$ (i.e., $a \leq y$ for all $a \in s$), then $x \leq y$.

subset_upperBounds_lowerBounds theorem

(s : Set α) : s ⊆ upperBounds (lowerBounds s)

Full source

theorem subset_upperBounds_lowerBounds (s : Set α) : s ⊆ upperBounds (lowerBounds s) :=
  fun _ hx _ hy => hy hx

Elements of a Set are Upper Bounds of its Lower Bounds

Informal description

For any subset $s$ of a partially ordered set $\alpha$, every element of $s$ is an upper bound for the set of lower bounds of $s$. In other words, if $x \in s$ and $y$ is a lower bound for $s$ (i.e., $y \leq a$ for all $a \in s$), then $y \leq x$.

Set.Nonempty.bddAbove_lowerBounds theorem

(hs : s.Nonempty) : BddAbove (lowerBounds s)

Full source

theorem Set.Nonempty.bddAbove_lowerBounds (hs : s.Nonempty) : BddAbove (lowerBounds s) :=
  hs.mono (subset_upperBounds_lowerBounds s)

Nonempty sets have upper-bounded lower bounds

Informal description

For any nonempty subset $s$ of a partially ordered set $\alpha$, the set of lower bounds of $s$ is bounded above.

Set.Nonempty.bddBelow_upperBounds theorem

(hs : s.Nonempty) : BddBelow (upperBounds s)

Full source

theorem Set.Nonempty.bddBelow_upperBounds (hs : s.Nonempty) : BddBelow (upperBounds s) :=
  hs.mono (subset_lowerBounds_upperBounds s)

Nonempty sets have lower-bounded upper bounds

Informal description

For any nonempty subset $s$ of a partially ordered set $\alpha$, the set of upper bounds of $s$ is bounded below.

IsLeast.isGLB theorem

(h : IsLeast s a) : IsGLB s a

Full source

theorem IsLeast.isGLB (h : IsLeast s a) : IsGLB s a :=
  ⟨h.2, fun _ hb => hb h.1⟩

Least Element Implies Greatest Lower Bound

Informal description

If an element $a$ is the least element of a set $s$ in a partially ordered type $\alpha$ (i.e., $a \in s$ and $a \leq x$ for all $x \in s$), then $a$ is also the greatest lower bound (infimum) of $s$.

IsGreatest.isLUB theorem

(h : IsGreatest s a) : IsLUB s a

Full source

theorem IsGreatest.isLUB (h : IsGreatest s a) : IsLUB s a :=
  ⟨h.2, fun _ hb => hb h.1⟩

Greatest Element Implies Least Upper Bound

Informal description

If an element $a$ is the greatest element of a set $s$ in a partially ordered type $\alpha$ (i.e., $a \in s$ and $a$ is an upper bound for $s$), then $a$ is also the least upper bound (supremum) of $s$.

IsLUB.upperBounds_eq theorem

(h : IsLUB s a) : upperBounds s = Ici a

Full source

theorem IsLUB.upperBounds_eq (h : IsLUB s a) : upperBounds s = Ici a :=
  Set.ext fun _ => ⟨fun hb => h.2 hb, fun hb => upperBounds_mono_mem hb h.1⟩

Characterization of Upper Bounds via Supremum: $\text{upperBounds}(s) = [a, \infty)$

Informal description

If $a$ is the least upper bound (supremum) of a set $s$ in a partially ordered type $\alpha$, then the set of upper bounds of $s$ is equal to the left-closed right-infinite interval $[a, \infty)$.

IsGLB.lowerBounds_eq theorem

(h : IsGLB s a) : lowerBounds s = Iic a

Full source

theorem IsGLB.lowerBounds_eq (h : IsGLB s a) : lowerBounds s = Iic a :=
  h.dual.upperBounds_eq

Characterization of Lower Bounds via Infimum: $\text{lowerBounds}(s) = (-\infty, a]$

Informal description

If an element $a$ is the greatest lower bound (infimum) of a set $s$ in a partially ordered type $\alpha$, then the set of lower bounds of $s$ is equal to the left-infinite right-closed interval $(-\infty, a]$.

IsLeast.lowerBounds_eq theorem

(h : IsLeast s a) : lowerBounds s = Iic a

Full source

theorem IsLeast.lowerBounds_eq (h : IsLeast s a) : lowerBounds s = Iic a :=
  h.isGLB.lowerBounds_eq

Characterization of Lower Bounds via Least Element: $\text{lowerBounds}(s) = (-\infty, a]$

Informal description

If an element $a$ is the least element of a set $s$ in a partially ordered type $\alpha$ (i.e., $a \in s$ and $a \leq x$ for all $x \in s$), then the set of lower bounds of $s$ is equal to the left-infinite right-closed interval $(-\infty, a]$.

IsGreatest.upperBounds_eq theorem

(h : IsGreatest s a) : upperBounds s = Ici a

Full source

theorem IsGreatest.upperBounds_eq (h : IsGreatest s a) : upperBounds s = Ici a :=
  h.isLUB.upperBounds_eq

Characterization of Upper Bounds via Greatest Element: $\text{upperBounds}(s) = [a, \infty)$

Informal description

If $a$ is the greatest element of a set $s$ in a partially ordered type $\alpha$ (i.e., $a \in s$ and $a$ is an upper bound for $s$), then the set of upper bounds of $s$ is equal to the left-closed right-infinite interval $[a, \infty)$.

IsGreatest.lt_iff theorem

(h : IsGreatest s a) : a < b ↔ ∀ x ∈ s, x < b

Full source

theorem IsGreatest.lt_iff (h : IsGreatest s a) : a < b ↔ ∀ x ∈ s, x < b :=
  ⟨fun hlt _x hx => (h.2 hx).trans_lt hlt, fun h' => h' _ h.1⟩

Characterization of Strict Upper Bounds via Greatest Element

Informal description

Let $s$ be a set in a partially ordered type $\alpha$, and let $a$ be the greatest element of $s$. Then for any element $b \in \alpha$, we have $a < b$ if and only if every element $x \in s$ satisfies $x < b$.

IsLeast.lt_iff theorem

(h : IsLeast s a) : b < a ↔ ∀ x ∈ s, b < x

Full source

theorem IsLeast.lt_iff (h : IsLeast s a) : b < a ↔ ∀ x ∈ s, b < x :=
  h.dual.lt_iff

Characterization of Strict Lower Bounds via Least Element: $b < a \leftrightarrow \forall x \in s, b < x$

Informal description

Let $s$ be a set in a partially ordered type $\alpha$, and let $a$ be the least element of $s$. Then for any element $b \in \alpha$, we have $b < a$ if and only if $b$ is a strict lower bound for $s$ (i.e., $b < x$ for all $x \in s$).

isLUB_le_iff theorem

(h : IsLUB s a) : a ≤ b ↔ b ∈ upperBounds s

Full source

theorem isLUB_le_iff (h : IsLUB s a) : a ≤ b ↔ b ∈ upperBounds s := by
  rw [h.upperBounds_eq]
  rfl

Supremum Comparison Criterion: $a \leq b \leftrightarrow b$ is an upper bound for $s$

Informal description

Let $s$ be a subset of a partially ordered set $\alpha$, and let $a$ be the least upper bound of $s$. Then for any element $b \in \alpha$, we have $a \leq b$ if and only if $b$ is an upper bound for $s$ (i.e., $x \leq b$ for all $x \in s$).

le_isGLB_iff theorem

(h : IsGLB s a) : b ≤ a ↔ b ∈ lowerBounds s

Full source

theorem le_isGLB_iff (h : IsGLB s a) : b ≤ a ↔ b ∈ lowerBounds s := by
  rw [h.lowerBounds_eq]
  rfl

Infimum Comparison Criterion: $b \leq a \leftrightarrow b$ is a lower bound for $s$

Informal description

Let $s$ be a subset of a partially ordered set $\alpha$, and let $a$ be the greatest lower bound (infimum) of $s$. Then for any element $b \in \alpha$, we have $b \leq a$ if and only if $b$ is a lower bound for $s$ (i.e., $b \leq x$ for all $x \in s$).

isLUB_iff_le_iff theorem

: IsLUB s a ↔ ∀ b, a ≤ b ↔ b ∈ upperBounds s

Full source

theorem isLUB_iff_le_iff : IsLUBIsLUB s a ↔ ∀ b, a ≤ b ↔ b ∈ upperBounds s :=
  ⟨fun h _ => isLUB_le_iff h, fun H => ⟨(H _).1 le_rfl, fun b hb => (H b).2 hb⟩⟩

Characterization of Least Upper Bound via Upper Bounds

Informal description

An element $a$ is the least upper bound (supremum) of a set $s$ in a partially ordered set if and only if for every element $b$, the inequality $a \leq b$ holds precisely when $b$ is an upper bound for $s$ (i.e., $x \leq b$ for all $x \in s$).

isGLB_iff_le_iff theorem

: IsGLB s a ↔ ∀ b, b ≤ a ↔ b ∈ lowerBounds s

Full source

theorem isGLB_iff_le_iff : IsGLBIsGLB s a ↔ ∀ b, b ≤ a ↔ b ∈ lowerBounds s :=
  @isLUB_iff_le_iff αᵒᵈ _ _ _

Characterization of Greatest Lower Bound via Lower Bounds

Informal description

An element $a$ is the greatest lower bound (infimum) of a set $s$ in a partially ordered set if and only if for every element $b$, the inequality $b \leq a$ holds precisely when $b$ is a lower bound for $s$ (i.e., $b \leq x$ for all $x \in s$).

IsLUB.bddAbove theorem

(h : IsLUB s a) : BddAbove s

Full source

/-- If `s` has a least upper bound, then it is bounded above. -/
theorem IsLUB.bddAbove (h : IsLUB s a) : BddAbove s :=
  ⟨a, h.1⟩

Least Upper Bound Implies Bounded Above

Informal description

If an element $a$ is the least upper bound of a set $s$ in a partially ordered type, then $s$ is bounded above.

IsGLB.bddBelow theorem

(h : IsGLB s a) : BddBelow s

Full source

/-- If `s` has a greatest lower bound, then it is bounded below. -/
theorem IsGLB.bddBelow (h : IsGLB s a) : BddBelow s :=
  ⟨a, h.1⟩

Greatest Lower Bound Implies Bounded Below

Informal description

If a set $s$ in a partially ordered type $\alpha$ has a greatest lower bound $a$, then $s$ is bounded below.

IsGreatest.bddAbove theorem

(h : IsGreatest s a) : BddAbove s

Full source

/-- If `s` has a greatest element, then it is bounded above. -/
theorem IsGreatest.bddAbove (h : IsGreatest s a) : BddAbove s :=
  ⟨a, h.2⟩

Greatest Element Implies Bounded Above

Informal description

If a set $s$ in a partially ordered type $\alpha$ has a greatest element $a$, then $s$ is bounded above. That is, there exists an element $x \in \alpha$ such that $y \leq x$ for all $y \in s$.

IsLeast.bddBelow theorem

(h : IsLeast s a) : BddBelow s

Full source

/-- If `s` has a least element, then it is bounded below. -/
theorem IsLeast.bddBelow (h : IsLeast s a) : BddBelow s :=
  ⟨a, h.2⟩

Existence of Least Element Implies Bounded Below

Informal description

If a set $s$ in a partially ordered type $\alpha$ has a least element $a$, then $s$ is bounded below. That is, there exists an element $x \in \alpha$ such that $x \leq y$ for all $y \in s$.

IsLeast.nonempty theorem

(h : IsLeast s a) : s.Nonempty

Full source

theorem IsLeast.nonempty (h : IsLeast s a) : s.Nonempty :=
  ⟨a, h.1⟩

Nonemptiness of Set with Least Element

Informal description

If $a$ is a least element of a set $s$ in a partially ordered type $\alpha$, then $s$ is nonempty.

IsGreatest.nonempty theorem

(h : IsGreatest s a) : s.Nonempty

Full source

theorem IsGreatest.nonempty (h : IsGreatest s a) : s.Nonempty :=
  ⟨a, h.1⟩

Nonemptiness of Set with Greatest Element

Informal description

If $a$ is a greatest element of a set $s$ in a partially ordered type $\alpha$, then $s$ is nonempty.

upperBounds_union theorem

: upperBounds (s ∪ t) = upperBounds s ∩ upperBounds t

Full source

@[simp]
theorem upperBounds_union : upperBounds (s ∪ t) = upperBoundsupperBounds s ∩ upperBounds t :=
  Subset.antisymm (fun _ hb => ⟨fun _ hx => hb (Or.inl hx), fun _ hx => hb (Or.inr hx)⟩)
    fun _ hb _ hx => hx.elim (fun hs => hb.1 hs) fun ht => hb.2 ht

Upper Bounds of Union Equals Intersection of Upper Bounds

Informal description

For any two sets $s$ and $t$ in a type $\alpha$ with a preorder, the set of upper bounds of their union $s \cup t$ is equal to the intersection of the upper bounds of $s$ and the upper bounds of $t$, i.e., \[ \text{upperBounds}(s \cup t) = \text{upperBounds}(s) \cap \text{upperBounds}(t). \]

lowerBounds_union theorem

: lowerBounds (s ∪ t) = lowerBounds s ∩ lowerBounds t

Full source

@[simp]
theorem lowerBounds_union : lowerBounds (s ∪ t) = lowerBoundslowerBounds s ∩ lowerBounds t :=
  @upperBounds_union αᵒᵈ _ s t

Lower Bounds of Union Equals Intersection of Lower Bounds

Informal description

For any two sets $s$ and $t$ in a type $\alpha$ with a preorder, the set of lower bounds of their union $s \cup t$ is equal to the intersection of the lower bounds of $s$ and the lower bounds of $t$, i.e., \[ \text{lowerBounds}(s \cup t) = \text{lowerBounds}(s) \cap \text{lowerBounds}(t). \]

union_upperBounds_subset_upperBounds_inter theorem

: upperBounds s ∪ upperBounds t ⊆ upperBounds (s ∩ t)

Full source

theorem union_upperBounds_subset_upperBounds_inter :
    upperBoundsupperBounds s ∪ upperBounds tupperBounds s ∪ upperBounds t ⊆ upperBounds (s ∩ t) :=
  union_subset (upperBounds_mono_set inter_subset_left)
    (upperBounds_mono_set inter_subset_right)

Union of Upper Bounds is Subset of Upper Bounds of Intersection

Informal description

For any two sets $s$ and $t$ in a preordered type $\alpha$, the union of their upper bounds is a subset of the upper bounds of their intersection, i.e., \[ \text{upperBounds}(s) \cup \text{upperBounds}(t) \subseteq \text{upperBounds}(s \cap t). \]

union_lowerBounds_subset_lowerBounds_inter theorem

: lowerBounds s ∪ lowerBounds t ⊆ lowerBounds (s ∩ t)

Full source

theorem union_lowerBounds_subset_lowerBounds_inter :
    lowerBoundslowerBounds s ∪ lowerBounds tlowerBounds s ∪ lowerBounds t ⊆ lowerBounds (s ∩ t) :=
  @union_upperBounds_subset_upperBounds_inter αᵒᵈ _ s t

Union of Lower Bounds is Subset of Lower Bounds of Intersection

Informal description

For any two sets $s$ and $t$ in a preordered type $\alpha$, the union of their lower bounds is a subset of the lower bounds of their intersection, i.e., \[ \text{lowerBounds}(s) \cup \text{lowerBounds}(t) \subseteq \text{lowerBounds}(s \cap t). \]

isLeast_union_iff theorem

 {a : α} {s t : Set α} : IsLeast (s ∪ t) a ↔ IsLeast s a ∧ a ∈ lowerBounds t ∨ a ∈ lowerBounds s ∧ IsLeast t a

Full source

theorem isLeast_union_iff {a : α} {s t : Set α} :
    IsLeastIsLeast (s ∪ t) a ↔ IsLeast s a ∧ a ∈ lowerBounds t ∨ a ∈ lowerBounds s ∧ IsLeast t a := by
  simp [IsLeast, lowerBounds_union, or_and_right, and_comm (a := a ∈ t), and_assoc]

Characterization of Least Element in Union: $\text{IsLeast}(s \cup t, a) \leftrightarrow (\text{IsLeast}(s, a) \land a \in \text{lowerBounds}(t)) \lor (a \in \text{lowerBounds}(s) \land \text{IsLeast}(t, a))$

Informal description

For any element $a$ in a partially ordered type $\alpha$ and any sets $s, t \subseteq \alpha$, the following are equivalent: 1. $a$ is the least element of $s \cup t$ 2. Either: - $a$ is the least element of $s$ and $a$ is a lower bound for $t$, or - $a$ is a lower bound for $s$ and $a$ is the least element of $t$. In other words, $a$ is the least element of $s \cup t$ if and only if it is the least element of one set while being a lower bound for the other.

isGreatest_union_iff theorem

: IsGreatest (s ∪ t) a ↔ IsGreatest s a ∧ a ∈ upperBounds t ∨ a ∈ upperBounds s ∧ IsGreatest t a

Full source

theorem isGreatest_union_iff :
    IsGreatestIsGreatest (s ∪ t) a ↔
      IsGreatest s a ∧ a ∈ upperBounds t ∨ a ∈ upperBounds s ∧ IsGreatest t a :=
  @isLeast_union_iff αᵒᵈ _ a s t

Characterization of Greatest Element in Union: $\text{IsGreatest}(s \cup t, a) \leftrightarrow (\text{IsGreatest}(s, a) \land a \in \text{upperBounds}(t)) \lor (a \in \text{upperBounds}(s) \land \text{IsGreatest}(t, a))$

Informal description

For any element $a$ in a partially ordered type $\alpha$ and any sets $s, t \subseteq \alpha$, the following are equivalent: 1. $a$ is the greatest element of $s \cup t$ 2. Either: - $a$ is the greatest element of $s$ and $a$ is an upper bound for $t$, or - $a$ is an upper bound for $s$ and $a$ is the greatest element of $t$. In other words, $a$ is the greatest element of $s \cup t$ if and only if it is the greatest element of one set while being an upper bound for the other.

BddAbove.inter_of_left theorem

(h : BddAbove s) : BddAbove (s ∩ t)

Full source

/-- If `s` is bounded, then so is `s ∩ t` -/
theorem BddAbove.inter_of_left (h : BddAbove s) : BddAbove (s ∩ t) :=
  h.mono inter_subset_left

Intersection with Bounded Above Set is Bounded Above

Informal description

If a set $s$ in a preordered type $\alpha$ is bounded above, then the intersection $s \cap t$ is also bounded above for any set $t \subseteq \alpha$.

BddAbove.inter_of_right theorem

(h : BddAbove t) : BddAbove (s ∩ t)

Full source

/-- If `t` is bounded, then so is `s ∩ t` -/
theorem BddAbove.inter_of_right (h : BddAbove t) : BddAbove (s ∩ t) :=
  h.mono inter_subset_right

Intersection with Bounded Above Set is Bounded Above (Right Version)

Informal description

If a set $t$ in a preordered type $\alpha$ is bounded above, then the intersection $s \cap t$ is also bounded above for any set $s \subseteq \alpha$.

BddBelow.inter_of_left theorem

(h : BddBelow s) : BddBelow (s ∩ t)

Full source

/-- If `s` is bounded, then so is `s ∩ t` -/
theorem BddBelow.inter_of_left (h : BddBelow s) : BddBelow (s ∩ t) :=
  h.mono inter_subset_left

Intersection with Bounded Below Set is Bounded Below

Informal description

If a set $s$ in a partially ordered type $\alpha$ is bounded below, then the intersection $s \cap t$ is also bounded below for any set $t \subseteq \alpha$.

BddBelow.inter_of_right theorem

(h : BddBelow t) : BddBelow (s ∩ t)

Full source

/-- If `t` is bounded, then so is `s ∩ t` -/
theorem BddBelow.inter_of_right (h : BddBelow t) : BddBelow (s ∩ t) :=
  h.mono inter_subset_right

Intersection with Bounded Below Set is Bounded Below (Right Version)

Informal description

If a set $t$ in a partially ordered type $\alpha$ is bounded below, then the intersection $s \cap t$ is also bounded below for any set $s \subseteq \alpha$.

BddAbove.union theorem

[IsDirected α (· ≤ ·)] {s t : Set α} : BddAbove s → BddAbove t → BddAbove (s ∪ t)

Full source

/-- In a directed order, the union of bounded above sets is bounded above. -/
theorem BddAbove.union [IsDirected α (· ≤ ·)] {s t : Set α} :
    BddAbove s → BddAbove t → BddAbove (s ∪ t) := by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  obtain ⟨c, hca, hcb⟩ := exists_ge_ge a b
  rw [BddAbove, upperBounds_union]
  exact ⟨c, upperBounds_mono_mem hca ha, upperBounds_mono_mem hcb hb⟩

Union of Bounded Above Sets is Bounded Above in Directed Orders

Informal description

Let $\alpha$ be a type with a directed order $\leq$. For any two sets $s, t \subseteq \alpha$ that are bounded above, their union $s \cup t$ is also bounded above.

bddAbove_union theorem

[IsDirected α (· ≤ ·)] {s t : Set α} : BddAbove (s ∪ t) ↔ BddAbove s ∧ BddAbove t

Full source

/-- In a directed order, the union of two sets is bounded above if and only if both sets are. -/
theorem bddAbove_union [IsDirected α (· ≤ ·)] {s t : Set α} :
    BddAboveBddAbove (s ∪ t) ↔ BddAbove s ∧ BddAbove t :=
  ⟨fun h => ⟨h.mono subset_union_left, h.mono subset_union_right⟩, fun h =>
    h.1.union h.2⟩

Union of Sets is Bounded Above if and Only if Each Set is Bounded Above in Directed Orders

Informal description

Let $\alpha$ be a type with a directed order $\leq$. For any two sets $s, t \subseteq \alpha$, the union $s \cup t$ is bounded above if and only if both $s$ and $t$ are bounded above.

BddBelow.union theorem

[IsDirected α (· ≥ ·)] {s t : Set α} : BddBelow s → BddBelow t → BddBelow (s ∪ t)

Full source

/-- In a codirected order, the union of bounded below sets is bounded below. -/
theorem BddBelow.union [IsDirected α (· ≥ ·)] {s t : Set α} :
    BddBelow s → BddBelow t → BddBelow (s ∪ t) :=
  @BddAbove.union αᵒᵈ _ _ _ _

Union of Bounded Below Sets is Bounded Below in Codirected Orders

Informal description

Let $\alpha$ be a type with a codirected order $\geq$ (i.e., $\leq$ is directed). For any two sets $s, t \subseteq \alpha$ that are bounded below, their union $s \cup t$ is also bounded below.

bddBelow_union theorem

[IsDirected α (· ≥ ·)] {s t : Set α} : BddBelow (s ∪ t) ↔ BddBelow s ∧ BddBelow t

Full source

/-- In a codirected order, the union of two sets is bounded below if and only if both sets are. -/
theorem bddBelow_union [IsDirected α (· ≥ ·)] {s t : Set α} :
    BddBelowBddBelow (s ∪ t) ↔ BddBelow s ∧ BddBelow t :=
  @bddAbove_union αᵒᵈ _ _ _ _

Union of Sets is Bounded Below if and Only if Each Set is Bounded Below in Codirected Orders

Informal description

Let $\alpha$ be a type with a codirected order $\geq$ (i.e., $\leq$ is directed). For any two sets $s, t \subseteq \alpha$, the union $s \cup t$ is bounded below if and only if both $s$ and $t$ are bounded below.

IsLUB.union theorem

[SemilatticeSup γ] {a b : γ} {s t : Set γ} (hs : IsLUB s a) (ht : IsLUB t b) : IsLUB (s ∪ t) (a ⊔ b)

Full source

/-- If `a` is the least upper bound of `s` and `b` is the least upper bound of `t`,
then `a ⊔ b` is the least upper bound of `s ∪ t`. -/
theorem IsLUB.union [SemilatticeSup γ] {a b : γ} {s t : Set γ} (hs : IsLUB s a) (ht : IsLUB t b) :
    IsLUB (s ∪ t) (a ⊔ b) :=
  ⟨fun _ h =>
    h.casesOn (fun h => le_sup_of_le_left <| hs.left h) fun h => le_sup_of_le_right <| ht.left h,
    fun _ hc =>
    sup_le (hs.right fun _ hd => hc <| Or.inl hd) (ht.right fun _ hd => hc <| Or.inr hd)⟩

Supremum of Union is Supremum of Suprema in Semilattices

Informal description

Let $\gamma$ be a type with a semilattice structure under the supremum operation $\sqcup$. For any two sets $s, t \subseteq \gamma$, if $a$ is the least upper bound of $s$ and $b$ is the least upper bound of $t$, then $a \sqcup b$ is the least upper bound of $s \cup t$.

IsGLB.union theorem

 [SemilatticeInf γ] {a₁ a₂ : γ} {s t : Set γ} (hs : IsGLB s a₁) (ht : IsGLB t a₂) : IsGLB (s ∪ t) (a₁ ⊓ a₂)

Full source

/-- If `a` is the greatest lower bound of `s` and `b` is the greatest lower bound of `t`,
then `a ⊓ b` is the greatest lower bound of `s ∪ t`. -/
theorem IsGLB.union [SemilatticeInf γ] {a₁ a₂ : γ} {s t : Set γ} (hs : IsGLB s a₁)
    (ht : IsGLB t a₂) : IsGLB (s ∪ t) (a₁ ⊓ a₂) :=
  hs.dual.union ht

Infimum of Union is Infimum of Infima in Semilattices

Informal description

Let $\gamma$ be a type with a semilattice structure under the infimum operation $\sqcap$. For any two sets $s, t \subseteq \gamma$, if $a_1$ is the greatest lower bound of $s$ and $a_2$ is the greatest lower bound of $t$, then $a_1 \sqcap a_2$ is the greatest lower bound of $s \cup t$.

IsLeast.union theorem

[LinearOrder γ] {a b : γ} {s t : Set γ} (ha : IsLeast s a) (hb : IsLeast t b) : IsLeast (s ∪ t) (min a b)

Full source

/-- If `a` is the least element of `s` and `b` is the least element of `t`,
then `min a b` is the least element of `s ∪ t`. -/
theorem IsLeast.union [LinearOrder γ] {a b : γ} {s t : Set γ} (ha : IsLeast s a)
    (hb : IsLeast t b) : IsLeast (s ∪ t) (min a b) :=
  ⟨by rcases le_total a b with h | h <;> simp [h, ha.1, hb.1], (ha.isGLB.union hb.isGLB).1⟩

Least Element of Union is Minimum of Least Elements in Linear Order

Informal description

Let $\gamma$ be a linearly ordered type, and let $s, t \subseteq \gamma$ be two subsets. If $a$ is the least element of $s$ and $b$ is the least element of $t$, then $\min(a, b)$ is the least element of the union $s \cup t$.

IsGreatest.union theorem

[LinearOrder γ] {a b : γ} {s t : Set γ} (ha : IsGreatest s a) (hb : IsGreatest t b) : IsGreatest (s ∪ t) (max a b)

Full source

/-- If `a` is the greatest element of `s` and `b` is the greatest element of `t`,
then `max a b` is the greatest element of `s ∪ t`. -/
theorem IsGreatest.union [LinearOrder γ] {a b : γ} {s t : Set γ} (ha : IsGreatest s a)
    (hb : IsGreatest t b) : IsGreatest (s ∪ t) (max a b) :=
  ⟨by rcases le_total a b with h | h <;> simp [h, ha.1, hb.1], (ha.isLUB.union hb.isLUB).1⟩

Greatest Element of Union is Maximum of Greatest Elements in Linear Order

Informal description

Let $\gamma$ be a linearly ordered type, and let $s, t \subseteq \gamma$ be two subsets. If $a$ is the greatest element of $s$ and $b$ is the greatest element of $t$, then $\max(a, b)$ is the greatest element of the union $s \cup t$.

IsLUB.inter_Ici_of_mem theorem

[LinearOrder γ] {s : Set γ} {a b : γ} (ha : IsLUB s a) (hb : b ∈ s) : IsLUB (s ∩ Ici b) a

Full source

theorem IsLUB.inter_Ici_of_mem [LinearOrder γ] {s : Set γ} {a b : γ} (ha : IsLUB s a) (hb : b ∈ s) :
    IsLUB (s ∩ Ici b) a :=
  ⟨fun _ hx => ha.1 hx.1, fun c hc =>
    have hbc : b ≤ c := hc ⟨hb, le_rfl⟩
    ha.2 fun x hx => ((le_total x b).elim fun hxb => hxb.trans hbc) fun hbx => hc ⟨hx, hbx⟩⟩

Least upper bound preserved under intersection with right-infinite interval containing a member

Informal description

Let $\gamma$ be a linearly ordered type, $s$ a subset of $\gamma$, and $a, b$ elements of $\gamma$. If $a$ is the least upper bound of $s$ and $b$ is an element of $s$, then $a$ is also the least upper bound of the intersection $s \cap [b, \infty)$.

IsGLB.inter_Iic_of_mem theorem

[LinearOrder γ] {s : Set γ} {a b : γ} (ha : IsGLB s a) (hb : b ∈ s) : IsGLB (s ∩ Iic b) a

Full source

theorem IsGLB.inter_Iic_of_mem [LinearOrder γ] {s : Set γ} {a b : γ} (ha : IsGLB s a) (hb : b ∈ s) :
    IsGLB (s ∩ Iic b) a :=
  ha.dual.inter_Ici_of_mem hb

Greatest lower bound preserved under intersection with left-infinite interval containing a member

Informal description

Let $\gamma$ be a linearly ordered type, $s$ a subset of $\gamma$, and $a, b$ elements of $\gamma$. If $a$ is the greatest lower bound of $s$ and $b$ is an element of $s$, then $a$ is also the greatest lower bound of the intersection $s \cap (-\infty, b]$.

bddAbove_iff_exists_ge theorem

[SemilatticeSup γ] {s : Set γ} (x₀ : γ) : BddAbove s ↔ ∃ x, x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x

Full source

theorem bddAbove_iff_exists_ge [SemilatticeSup γ] {s : Set γ} (x₀ : γ) :
    BddAboveBddAbove s ↔ ∃ x, x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x := by
  rw [bddAbove_def, exists_ge_and_iff_exists]
  exact Monotone.ball fun x _ => monotone_le

Characterization of Bounded Above Sets via Existence of Upper Bound Greater Than a Given Element

Informal description

Let $\gamma$ be a type with a semilattice structure under the supremum operation, and let $s$ be a subset of $\gamma$. For any element $x_0 \in \gamma$, the set $s$ is bounded above if and only if there exists an element $x \in \gamma$ such that $x_0 \leq x$ and $x$ is an upper bound for $s$ (i.e., $y \leq x$ for all $y \in s$).

bddBelow_iff_exists_le theorem

[SemilatticeInf γ] {s : Set γ} (x₀ : γ) : BddBelow s ↔ ∃ x, x ≤ x₀ ∧ ∀ y ∈ s, x ≤ y

Full source

theorem bddBelow_iff_exists_le [SemilatticeInf γ] {s : Set γ} (x₀ : γ) :
    BddBelowBddBelow s ↔ ∃ x, x ≤ x₀ ∧ ∀ y ∈ s, x ≤ y :=
  bddAbove_iff_exists_ge (toDual x₀)

Characterization of Bounded Below Sets via Existence of Lower Bound Less Than a Given Element

Informal description

Let $\gamma$ be a type with a semilattice structure under the infimum operation, and let $s$ be a subset of $\gamma$. For any element $x_0 \in \gamma$, the set $s$ is bounded below if and only if there exists an element $x \in \gamma$ such that $x \leq x_0$ and $x$ is a lower bound for $s$ (i.e., $x \leq y$ for all $y \in s$).

BddAbove.exists_ge theorem

[SemilatticeSup γ] {s : Set γ} (hs : BddAbove s) (x₀ : γ) : ∃ x, x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x

Full source

theorem BddAbove.exists_ge [SemilatticeSup γ] {s : Set γ} (hs : BddAbove s) (x₀ : γ) :
    ∃ x, x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x :=
  (bddAbove_iff_exists_ge x₀).mp hs

Existence of Upper Bound Greater Than Given Element for Bounded Above Sets

Informal description

Let $\gamma$ be a type with a semilattice structure under the supremum operation, and let $s$ be a subset of $\gamma$ that is bounded above. For any element $x_0 \in \gamma$, there exists an element $x \in \gamma$ such that $x_0 \leq x$ and $x$ is an upper bound for $s$ (i.e., $y \leq x$ for all $y \in s$).

BddBelow.exists_le theorem

[SemilatticeInf γ] {s : Set γ} (hs : BddBelow s) (x₀ : γ) : ∃ x, x ≤ x₀ ∧ ∀ y ∈ s, x ≤ y

Full source

theorem BddBelow.exists_le [SemilatticeInf γ] {s : Set γ} (hs : BddBelow s) (x₀ : γ) :
    ∃ x, x ≤ x₀ ∧ ∀ y ∈ s, x ≤ y :=
  (bddBelow_iff_exists_le x₀).mp hs

Existence of Lower Bound Less Than Given Element for Bounded Below Sets

Informal description

Let $\gamma$ be a type with a semilattice structure under the infimum operation, and let $s$ be a subset of $\gamma$ that is bounded below. For any element $x_0 \in \gamma$, there exists an element $x \in \gamma$ such that $x \leq x_0$ and $x$ is a lower bound for $s$ (i.e., $x \leq y$ for all $y \in s$).

isLeast_Ici theorem

: IsLeast (Ici a) a

Full source

theorem isLeast_Ici : IsLeast (Ici a) a :=
  ⟨left_mem_Ici, fun _ => id⟩

Least element property of $[a, \infty)$

Informal description

For any element $a$ in a preorder, $a$ is the least element of the left-closed right-infinite interval $[a, \infty)$, meaning $a \in [a, \infty)$ and $a$ is a lower bound for this interval (i.e., $a \leq x$ for all $x \in [a, \infty)$).

isGreatest_Iic theorem

: IsGreatest (Iic a) a

Full source

theorem isGreatest_Iic : IsGreatest (Iic a) a :=
  ⟨right_mem_Iic, fun _ => id⟩

Greatest element of right-closed interval $(-\infty, a]$ is $a$

Informal description

For any element $a$ in a preorder, $a$ is the greatest element of the left-infinite right-closed interval $(-\infty, a]$, meaning $a \in (-\infty, a]$ and $a$ is an upper bound for this interval (i.e., $x \leq a$ for all $x \in (-\infty, a]$).

isLUB_Iic theorem

: IsLUB (Iic a) a

Full source

theorem isLUB_Iic : IsLUB (Iic a) a :=
  isGreatest_Iic.isLUB

Least Upper Bound Property of $(-\infty, a]$

Informal description

For any element $a$ in a preorder, $a$ is the least upper bound (supremum) of the left-infinite right-closed interval $(-\infty, a]$. That is, $a$ is an upper bound for $(-\infty, a]$ (i.e., $x \leq a$ for all $x \leq a$) and is less than or equal to any other upper bound of $(-\infty, a]$.

isGLB_Ici theorem

: IsGLB (Ici a) a

Full source

theorem isGLB_Ici : IsGLB (Ici a) a :=
  isLeast_Ici.isGLB

Greatest lower bound property of $[a, \infty)$

Informal description

For any element $a$ in a preorder, $a$ is the greatest lower bound (infimum) of the left-closed right-infinite interval $[a, \infty)$. That is, $a$ is a lower bound for $[a, \infty)$ (i.e., $a \leq x$ for all $x \geq a$) and is greater than or equal to any other lower bound of $[a, \infty)$.

upperBounds_Iic theorem

: upperBounds (Iic a) = Ici a

Full source

theorem upperBounds_Iic : upperBounds (Iic a) = Ici a :=
  isLUB_Iic.upperBounds_eq

Upper Bounds of $(-\infty, a]$ Equal $[a, \infty)$

Informal description

For any element $a$ in a preorder, the set of upper bounds of the left-infinite right-closed interval $(-\infty, a]$ is equal to the left-closed right-infinite interval $[a, \infty)$. That is, $\text{upperBounds}((-\infty, a]) = [a, \infty)$.

lowerBounds_Ici theorem

: lowerBounds (Ici a) = Iic a

Full source

theorem lowerBounds_Ici : lowerBounds (Ici a) = Iic a :=
  isGLB_Ici.lowerBounds_eq

Lower Bounds of $[a, \infty)$ Equal $(-\infty, a]$

Informal description

For any element $a$ in a preorder, the set of lower bounds of the left-closed right-infinite interval $[a, \infty)$ is equal to the left-infinite right-closed interval $(-\infty, a]$. That is, $\text{lowerBounds}([a, \infty)) = (-\infty, a]$.

bddAbove_Iic theorem

: BddAbove (Iic a)

Full source

theorem bddAbove_Iic : BddAbove (Iic a) :=
  isLUB_Iic.bddAbove

Left-infinite right-closed interval is bounded above

Informal description

For any element $a$ in a preorder $\alpha$, the left-infinite right-closed interval $(-\infty, a]$ is bounded above.

bddBelow_Ici theorem

: BddBelow (Ici a)

Full source

theorem bddBelow_Ici : BddBelow (Ici a) :=
  isGLB_Ici.bddBelow

Left-closed interval is bounded below

Informal description

For any element $a$ in a preorder $\alpha$, the left-closed right-infinite interval $[a, \infty)$ is bounded below.

bddAbove_Iio theorem

: BddAbove (Iio a)

Full source

theorem bddAbove_Iio : BddAbove (Iio a) :=
  ⟨a, fun _ hx => le_of_lt hx⟩

Left-infinite interval is bounded above

Informal description

For any element $a$ in a preorder $\alpha$, the left-infinite right-open interval $(-\infty, a)$ is bounded above.

bddBelow_Ioi theorem

: BddBelow (Ioi a)

Full source

theorem bddBelow_Ioi : BddBelow (Ioi a) :=
  ⟨a, fun _ hx => le_of_lt hx⟩

Left-open interval is bounded below

Informal description

For any element $a$ in a preorder $\alpha$, the left-open right-infinite interval $(a, \infty)$ is bounded below.

lub_Iio_le theorem

(a : α) (hb : IsLUB (Iio a) b) : b ≤ a

Full source

theorem lub_Iio_le (a : α) (hb : IsLUB (Iio a) b) : b ≤ a :=
  (isLUB_le_iff hb).mpr fun _ hk => le_of_lt hk

Supremum of $(-\infty, a)$ is bounded above by $a$

Informal description

For any element $a$ in a preorder $\alpha$, if $b$ is the least upper bound of the left-infinite right-open interval $(-\infty, a)$, then $b \leq a$.

le_glb_Ioi theorem

(a : α) (hb : IsGLB (Ioi a) b) : a ≤ b

Full source

theorem le_glb_Ioi (a : α) (hb : IsGLB (Ioi a) b) : a ≤ b :=
  @lub_Iio_le αᵒᵈ _ _ a hb

Greatest lower bound of $(a, \infty)$ is bounded below by $a$

Informal description

For any element $a$ in a preorder $\alpha$, if $b$ is the greatest lower bound of the left-open right-infinite interval $(a, \infty)$, then $a \leq b$.

lub_Iio_eq_self_or_Iio_eq_Iic theorem

[PartialOrder γ] {j : γ} (i : γ) (hj : IsLUB (Iio i) j) : j = i ∨ Iio i = Iic j

Full source

theorem lub_Iio_eq_self_or_Iio_eq_Iic [PartialOrder γ] {j : γ} (i : γ) (hj : IsLUB (Iio i) j) :
    j = i ∨ Iio i = Iic j := by
  rcases eq_or_lt_of_le (lub_Iio_le i hj) with hj_eq_i | hj_lt_i
  · exact Or.inl hj_eq_i
  · right
    exact Set.ext fun k => ⟨fun hk_lt => hj.1 hk_lt, fun hk_le_j => lt_of_le_of_lt hk_le_j hj_lt_i⟩

Supremum Characterization for Left-Infinite Right-Open Interval in Partial Orders

Informal description

Let $\gamma$ be a partially ordered set, and let $i, j \in \gamma$ such that $j$ is the least upper bound of the left-infinite right-open interval $(-\infty, i)$. Then either $j = i$, or the interval $(-\infty, i)$ is equal to the left-infinite right-closed interval $(-\infty, j]$.

glb_Ioi_eq_self_or_Ioi_eq_Ici theorem

[PartialOrder γ] {j : γ} (i : γ) (hj : IsGLB (Ioi i) j) : j = i ∨ Ioi i = Ici j

Full source

theorem glb_Ioi_eq_self_or_Ioi_eq_Ici [PartialOrder γ] {j : γ} (i : γ) (hj : IsGLB (Ioi i) j) :
    j = i ∨ Ioi i = Ici j :=
  @lub_Iio_eq_self_or_Iio_eq_Iic γᵒᵈ _ j i hj

Infimum Characterization for Left-Open Right-Infinite Interval in Partial Orders

Informal description

Let $\gamma$ be a partially ordered set, and let $i, j \in \gamma$ such that $j$ is the greatest lower bound of the left-open right-infinite interval $(i, \infty)$. Then either $j = i$, or the interval $(i, \infty)$ is equal to the left-closed right-infinite interval $[j, \infty)$.

exists_lub_Iio theorem

(i : γ) : ∃ j, IsLUB (Iio i) j

Full source

theorem exists_lub_Iio (i : γ) : ∃ j, IsLUB (Iio i) j := by
  by_cases h_exists_lt : ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
  · obtain ⟨j, hj_ub, hj_lt_i⟩ := h_exists_lt
    exact ⟨j, hj_ub, fun k hk_ub => hk_ub hj_lt_i⟩
  · refine ⟨i, fun j hj => le_of_lt hj, ?_⟩
    rw [mem_lowerBounds]
    by_contra h
    refine h_exists_lt ?_
    push_neg at h
    exact h

Existence of Supremum for Left-Infinite Right-Open Interval

Informal description

For any element $i$ in a partially ordered type $\gamma$, there exists an element $j \in \gamma$ that is the least upper bound (supremum) of the left-infinite right-open interval $(-\infty, i)$, i.e., $\exists j, \operatorname{IsLUB}(\{x \mid x < i\}, j)$.

exists_glb_Ioi theorem

(i : γ) : ∃ j, IsGLB (Ioi i) j

Full source

theorem exists_glb_Ioi (i : γ) : ∃ j, IsGLB (Ioi i) j :=
  @exists_lub_Iio γᵒᵈ _ i

Existence of Infimum for Left-Open Right-Infinite Interval

Informal description

For any element $i$ in a partially ordered type $\gamma$, there exists an element $j \in \gamma$ that is the greatest lower bound (infimum) of the left-open right-infinite interval $(i, \infty)$, i.e., $\exists j, \operatorname{IsGLB}(\{x \mid i < x\}, j)$.

isLUB_Iio theorem

{a : γ} : IsLUB (Iio a) a

Full source

theorem isLUB_Iio {a : γ} : IsLUB (Iio a) a :=
  ⟨fun _ hx => le_of_lt hx, fun _ hy => le_of_forall_lt_imp_le_of_dense hy⟩

$a$ is the supremum of $(-\infty, a)$

Informal description

For any element $a$ in a partially ordered type $\gamma$, the element $a$ is the least upper bound (supremum) of the left-infinite right-open interval $(-\infty, a)$, i.e., $\operatorname{IsLUB}(\{x \mid x < a\}, a)$.

isGLB_Ioi theorem

{a : γ} : IsGLB (Ioi a) a

Full source

theorem isGLB_Ioi {a : γ} : IsGLB (Ioi a) a :=
  @isLUB_Iio γᵒᵈ _ _ a

$a$ is the infimum of $(a, \infty)$

Informal description

For any element $a$ in a partially ordered type $\gamma$, the element $a$ is the greatest lower bound (infimum) of the left-open right-infinite interval $(a, \infty)$, i.e., $\operatorname{IsGLB}(\{x \mid a < x\}, a)$.

upperBounds_Iio theorem

{a : γ} : upperBounds (Iio a) = Ici a

Full source

theorem upperBounds_Iio {a : γ} : upperBounds (Iio a) = Ici a :=
  isLUB_Iio.upperBounds_eq

Upper Bounds of $(-\infty, a)$ Equal $[a, \infty)$

Informal description

For any element $a$ in a partially ordered type $\gamma$, the set of upper bounds of the left-infinite right-open interval $(-\infty, a)$ is equal to the left-closed right-infinite interval $[a, \infty)$. In other words, $\text{upperBounds}(\{x \mid x < a\}) = \{y \mid a \leq y\}$.

lowerBounds_Ioi theorem

{a : γ} : lowerBounds (Ioi a) = Iic a

Full source

theorem lowerBounds_Ioi {a : γ} : lowerBounds (Ioi a) = Iic a :=
  isGLB_Ioi.lowerBounds_eq

Lower Bounds of $(a, \infty)$ Equal $(-\infty, a]$

Informal description

For any element $a$ in a partially ordered type $\gamma$, the set of lower bounds of the left-open right-infinite interval $(a, \infty)$ is equal to the left-infinite right-closed interval $(-\infty, a]$. In other words, $\text{lowerBounds}(\{x \mid a < x\}) = \{y \mid y \leq a\}$.

isGreatest_singleton theorem

: IsGreatest { a } a

Full source

@[simp] theorem isGreatest_singleton : IsGreatest {a} a :=
  ⟨mem_singleton a, fun _ hx => le_of_eq <| eq_of_mem_singleton hx⟩

Greatest Element of a Singleton Set

Informal description

For any element $a$ in a partially ordered type $\alpha$, the singleton set $\{a\}$ has $a$ as its greatest element, i.e., $a \in \{a\}$ and $x \leq a$ for all $x \in \{a\}$.

isLeast_singleton theorem

: IsLeast { a } a

Full source

@[simp] theorem isLeast_singleton : IsLeast {a} a :=
  @isGreatest_singleton αᵒᵈ _ a

Least Element of a Singleton Set

Informal description

For any element $a$ in a partially ordered type $\alpha$, the singleton set $\{a\}$ has $a$ as its least element, i.e., $a \in \{a\}$ and $a \leq x$ for all $x \in \{a\}$.

isLUB_singleton theorem

: IsLUB { a } a

Full source

@[simp] theorem isLUB_singleton : IsLUB {a} a :=
  isGreatest_singleton.isLUB

Least Upper Bound of a Singleton Set is the Element Itself

Informal description

For any element $a$ in a partially ordered type $\alpha$, the singleton set $\{a\}$ has $a$ as its least upper bound (supremum), i.e., $a$ is an upper bound for $\{a\}$ and is less than or equal to any other upper bound of $\{a\}$.

isGLB_singleton theorem

: IsGLB { a } a

Full source

@[simp] theorem isGLB_singleton : IsGLB {a} a :=
  isLeast_singleton.isGLB

Greatest Lower Bound of a Singleton Set is the Element Itself

Informal description

For any element $a$ in a partially ordered type $\alpha$, the singleton set $\{a\}$ has $a$ as its greatest lower bound (infimum).

bddAbove_singleton theorem

: BddAbove ({ a } : Set α)

Full source

@[simp] lemma bddAbove_singleton : BddAbove ({a} : Set α) := isLUB_singleton.bddAbove

Singleton Sets are Bounded Above

Informal description

For any element $a$ in a type $\alpha$ with a preorder, the singleton set $\{a\}$ is bounded above.

bddBelow_singleton theorem

: BddBelow ({ a } : Set α)

Full source

@[simp] lemma bddBelow_singleton : BddBelow ({a} : Set α) := isGLB_singleton.bddBelow

Singleton Sets are Bounded Below

Informal description

For any element $a$ in a partially ordered type $\alpha$, the singleton set $\{a\}$ is bounded below.

upperBounds_singleton theorem

: upperBounds { a } = Ici a

Full source

@[simp]
theorem upperBounds_singleton : upperBounds {a} = Ici a :=
  isLUB_singleton.upperBounds_eq

Upper Bounds of Singleton Set: $\text{upperBounds}(\{a\}) = [a, \infty)$

Informal description

For any element $a$ in a preordered type $\alpha$, the set of upper bounds of the singleton set $\{a\}$ is equal to the left-closed right-infinite interval $[a, \infty)$.

lowerBounds_singleton theorem

: lowerBounds { a } = Iic a

Full source

@[simp]
theorem lowerBounds_singleton : lowerBounds {a} = Iic a :=
  isGLB_singleton.lowerBounds_eq

Lower Bounds of Singleton Set: $\text{lowerBounds}(\{a\}) = (-\infty, a]$

Informal description

For any element $a$ in a partially ordered type $\alpha$, the set of lower bounds of the singleton set $\{a\}$ is equal to the left-infinite right-closed interval $(-\infty, a]$, i.e., $\text{lowerBounds}(\{a\}) = (-\infty, a]$.

bddAbove_Icc theorem

: BddAbove (Icc a b)

Full source

theorem bddAbove_Icc : BddAbove (Icc a b) :=
  ⟨b, fun _ => And.right⟩

Closed intervals are bounded above

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the closed interval $[a, b]$ is bounded above.

bddBelow_Icc theorem

: BddBelow (Icc a b)

Full source

theorem bddBelow_Icc : BddBelow (Icc a b) :=
  ⟨a, fun _ => And.left⟩

Closed intervals are bounded below

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the closed interval $[a, b]$ is bounded below.

bddAbove_Ico theorem

: BddAbove (Ico a b)

Full source

theorem bddAbove_Ico : BddAbove (Ico a b) :=
  bddAbove_Icc.mono Ico_subset_Icc_self

Left-Closed Right-Open Intervals are Bounded Above

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-closed right-open interval $[a, b)$ is bounded above.

bddBelow_Ico theorem

: BddBelow (Ico a b)

Full source

theorem bddBelow_Ico : BddBelow (Ico a b) :=
  bddBelow_Icc.mono Ico_subset_Icc_self

Left-closed right-open intervals are bounded below

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-closed right-open interval $[a, b)$ is bounded below.

bddAbove_Ioc theorem

: BddAbove (Ioc a b)

Full source

theorem bddAbove_Ioc : BddAbove (Ioc a b) :=
  bddAbove_Icc.mono Ioc_subset_Icc_self

Left-open right-closed intervals are bounded above

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-open right-closed interval $(a, b]$ is bounded above.

bddBelow_Ioc theorem

: BddBelow (Ioc a b)

Full source

theorem bddBelow_Ioc : BddBelow (Ioc a b) :=
  bddBelow_Icc.mono Ioc_subset_Icc_self

Left-open right-closed intervals are bounded below

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-open right-closed interval $(a, b]$ is bounded below.

bddAbove_Ioo theorem

: BddAbove (Ioo a b)

Full source

theorem bddAbove_Ioo : BddAbove (Ioo a b) :=
  bddAbove_Icc.mono Ioo_subset_Icc_self

Open Interval is Bounded Above: $(a, b)$ has an upper bound

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the open interval $(a, b)$ is bounded above.

bddBelow_Ioo theorem

: BddBelow (Ioo a b)

Full source

theorem bddBelow_Ioo : BddBelow (Ioo a b) :=
  bddBelow_Icc.mono Ioo_subset_Icc_self

Open Interval is Bounded Below: $(a, b)$ has a lower bound

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the open interval $(a, b)$ is bounded below.

isGreatest_Icc theorem

(h : a ≤ b) : IsGreatest (Icc a b) b

Full source

theorem isGreatest_Icc (h : a ≤ b) : IsGreatest (Icc a b) b :=
  ⟨right_mem_Icc.2 h, fun _ => And.right⟩

Greatest Element of Closed Interval: $b$ is greatest in $[a, b]$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder such that $a \leq b$, the element $b$ is the greatest element of the closed interval $[a, b]$, meaning $b \in [a, b]$ and $x \leq b$ for all $x \in [a, b]$.

isLUB_Icc theorem

(h : a ≤ b) : IsLUB (Icc a b) b

Full source

theorem isLUB_Icc (h : a ≤ b) : IsLUB (Icc a b) b :=
  (isGreatest_Icc h).isLUB

Least Upper Bound of Closed Interval: $b$ is supremum of $[a, b]$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder such that $a \leq b$, the element $b$ is the least upper bound (supremum) of the closed interval $[a, b]$. This means that $b$ is an upper bound for $[a, b]$ (i.e., $x \leq b$ for all $x \in [a, b]$) and is less than or equal to any other upper bound of $[a, b]$.

upperBounds_Icc theorem

(h : a ≤ b) : upperBounds (Icc a b) = Ici b

Full source

theorem upperBounds_Icc (h : a ≤ b) : upperBounds (Icc a b) = Ici b :=
  (isLUB_Icc h).upperBounds_eq

Upper Bounds of Closed Interval: $\text{upperBounds}([a, b]) = [b, \infty)$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder such that $a \leq b$, the set of upper bounds of the closed interval $[a, b]$ is equal to the left-closed right-infinite interval $[b, \infty)$.

isLeast_Icc theorem

(h : a ≤ b) : IsLeast (Icc a b) a

Full source

theorem isLeast_Icc (h : a ≤ b) : IsLeast (Icc a b) a :=
  ⟨left_mem_Icc.2 h, fun _ => And.left⟩

Least Element of Closed Interval: $a$ is Least in $[a, b]$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ with $a \leq b$, the element $a$ is the least element of the closed interval $[a, b]$, meaning $a \in [a, b]$ and $a \leq x$ for all $x \in [a, b]$.

isGLB_Icc theorem

(h : a ≤ b) : IsGLB (Icc a b) a

Full source

theorem isGLB_Icc (h : a ≤ b) : IsGLB (Icc a b) a :=
  (isLeast_Icc h).isGLB

Greatest Lower Bound of Closed Interval: $a$ is Infimum of $[a, b]$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ with $a \leq b$, the element $a$ is the greatest lower bound (infimum) of the closed interval $[a, b]$. This means that $a$ is a lower bound for $[a, b]$ (i.e., $a \leq x$ for all $x \in [a, b]$) and is greater than or equal to any other lower bound of $[a, b]$.

lowerBounds_Icc theorem

(h : a ≤ b) : lowerBounds (Icc a b) = Iic a

Full source

theorem lowerBounds_Icc (h : a ≤ b) : lowerBounds (Icc a b) = Iic a :=
  (isGLB_Icc h).lowerBounds_eq

Lower Bounds of Closed Interval: $\text{lowerBounds}([a, b]) = (-\infty, a]$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ with $a \leq b$, the set of lower bounds of the closed interval $[a, b]$ is equal to the left-infinite right-closed interval $(-\infty, a]$. In other words, $\text{lowerBounds}([a, b]) = (-\infty, a]$.

isGreatest_Ioc theorem

(h : a < b) : IsGreatest (Ioc a b) b

Full source

theorem isGreatest_Ioc (h : a < b) : IsGreatest (Ioc a b) b :=
  ⟨right_mem_Ioc.2 h, fun _ => And.right⟩

Greatest Element Property of Left-Open Right-Closed Interval: $b$ is greatest in $(a, b]$ when $a < b$

Informal description

For any elements $a$ and $b$ in a preorder with $a < b$, the element $b$ is the greatest element of the left-open right-closed interval $(a, b]$. That is, $b \in (a, b]$ and for all $x \in (a, b]$, we have $x \leq b$.

isLUB_Ioc theorem

(h : a < b) : IsLUB (Ioc a b) b

Full source

theorem isLUB_Ioc (h : a < b) : IsLUB (Ioc a b) b :=
  (isGreatest_Ioc h).isLUB

Least Upper Bound Property of Left-Open Right-Closed Interval: $\sup (a, b] = b$ when $a < b$

Informal description

For any elements $a$ and $b$ in a preorder with $a < b$, the element $b$ is the least upper bound (supremum) of the left-open right-closed interval $(a, b]$. That is, $b$ is an upper bound for $(a, b]$, and for any other upper bound $u$ of $(a, b]$, we have $b \leq u$.

upperBounds_Ioc theorem

(h : a < b) : upperBounds (Ioc a b) = Ici b

Full source

theorem upperBounds_Ioc (h : a < b) : upperBounds (Ioc a b) = Ici b :=
  (isLUB_Ioc h).upperBounds_eq

Characterization of Upper Bounds for $(a, b]$: $\text{upperBounds}((a, b]) = [b, \infty)$ when $a < b$

Informal description

For any elements $a$ and $b$ in a preorder with $a < b$, the set of upper bounds of the left-open right-closed interval $(a, b]$ is equal to the left-closed right-infinite interval $[b, \infty)$. That is, $\text{upperBounds}((a, b]) = [b, \infty)$.

isLeast_Ico theorem

(h : a < b) : IsLeast (Ico a b) a

Full source

theorem isLeast_Ico (h : a < b) : IsLeast (Ico a b) a :=
  ⟨left_mem_Ico.2 h, fun _ => And.left⟩

Least Element Property of Left-Closed Right-Open Interval: $a$ is least in $[a, b)$ when $a < b$

Informal description

For any elements $a$ and $b$ in a preorder with $a < b$, the element $a$ is the least element of the left-closed right-open interval $[a, b)$. That is, $a \in [a, b)$ and $a \leq x$ for all $x \in [a, b)$.

isGLB_Ico theorem

(h : a < b) : IsGLB (Ico a b) a

Full source

theorem isGLB_Ico (h : a < b) : IsGLB (Ico a b) a :=
  (isLeast_Ico h).isGLB

Infimum of $[a, b)$ is $a$ when $a < b$

Informal description

For any elements $a$ and $b$ in a partially ordered type with $a < b$, the element $a$ is the greatest lower bound (infimum) of the left-closed right-open interval $[a, b) = \{x \mid a \leq x < b\}$.

lowerBounds_Ico theorem

(h : a < b) : lowerBounds (Ico a b) = Iic a

Full source

theorem lowerBounds_Ico (h : a < b) : lowerBounds (Ico a b) = Iic a :=
  (isGLB_Ico h).lowerBounds_eq

Lower Bounds of $[a, b)$ Interval: $\text{lowerBounds}([a, b)) = (-\infty, a]$ when $a < b$

Informal description

For any elements $a$ and $b$ in a partially ordered type with $a < b$, the set of lower bounds of the left-closed right-open interval $[a, b)$ is equal to the left-infinite right-closed interval $(-\infty, a]$. In other words, $\text{lowerBounds}([a, b)) = (-\infty, a]$.

isGLB_Ioo theorem

{a b : γ} (h : a < b) : IsGLB (Ioo a b) a

Full source

theorem isGLB_Ioo {a b : γ} (h : a < b) : IsGLB (Ioo a b) a :=
  ⟨fun _ hx => hx.1.le, fun x hx => by
    rcases eq_or_lt_of_le (le_sup_right : a ≤ x ⊔ a) with h₁ | h₂
    · exact h₁.symm ▸ le_sup_left
    obtain ⟨y, lty, ylt⟩ := exists_between h₂
    apply (not_lt_of_le (sup_le (hx ⟨lty, ylt.trans_le (sup_le _ h.le)⟩) lty.le) ylt).elim
    obtain ⟨u, au, ub⟩ := exists_between h
    apply (hx ⟨au, ub⟩).trans ub.le⟩

$a$ is the infimum of the open interval $(a, b)$ when $a < b$

Informal description

For any elements $a$ and $b$ in a partially ordered type $\gamma$ with $a < b$, the element $a$ is the greatest lower bound (infimum) of the open interval $(a, b) = \{x \in \gamma \mid a < x < b\}$.

lowerBounds_Ioo theorem

{a b : γ} (hab : a < b) : lowerBounds (Ioo a b) = Iic a

Full source

theorem lowerBounds_Ioo {a b : γ} (hab : a < b) : lowerBounds (Ioo a b) = Iic a :=
  (isGLB_Ioo hab).lowerBounds_eq

Lower Bounds of Open Interval $(a, b)$ Equal $(-\infty, a]$

Informal description

For any elements $a$ and $b$ in a partially ordered type $\gamma$ with $a < b$, the set of lower bounds of the open interval $(a, b) = \{x \in \gamma \mid a < x < b\}$ is equal to the left-infinite right-closed interval $(-\infty, a] = \{x \in \gamma \mid x \leq a\}$.

isGLB_Ioc theorem

{a b : γ} (hab : a < b) : IsGLB (Ioc a b) a

Full source

theorem isGLB_Ioc {a b : γ} (hab : a < b) : IsGLB (Ioc a b) a :=
  (isGLB_Ioo hab).of_subset_of_superset (isGLB_Icc hab.le) Ioo_subset_Ioc_self Ioc_subset_Icc_self

$a$ is the infimum of $(a, b]$ when $a < b$

Informal description

For any elements $a$ and $b$ in a partially ordered type $\gamma$ with $a < b$, the element $a$ is the greatest lower bound (infimum) of the left-open right-closed interval $(a, b] = \{x \in \gamma \mid a < x \leq b\}$.

lowerBounds_Ioc theorem

{a b : γ} (hab : a < b) : lowerBounds (Ioc a b) = Iic a

Full source

theorem lowerBounds_Ioc {a b : γ} (hab : a < b) : lowerBounds (Ioc a b) = Iic a :=
  (isGLB_Ioc hab).lowerBounds_eq

Lower Bounds of $(a, b]$ Equal $(-\infty, a]$ When $a < b$

Informal description

For any elements $a$ and $b$ in a partially ordered type $\gamma$ with $a < b$, the set of lower bounds of the left-open right-closed interval $(a, b] = \{x \in \gamma \mid a < x \leq b\}$ is equal to the left-infinite right-closed interval $(-\infty, a] = \{x \in \gamma \mid x \leq a\}$.

isLUB_Ioo theorem

{a b : γ} (hab : a < b) : IsLUB (Ioo a b) b

Full source

theorem isLUB_Ioo {a b : γ} (hab : a < b) : IsLUB (Ioo a b) b := by
  simpa only [Ioo_toDual] using isGLB_Ioo hab.dual

$b$ is the supremum of the open interval $(a, b)$ when $a < b$

Informal description

For any elements $a$ and $b$ in a partially ordered type $\gamma$ with $a < b$, the element $b$ is the least upper bound (supremum) of the open interval $(a, b) = \{x \in \gamma \mid a < x < b\}$.

upperBounds_Ioo theorem

{a b : γ} (hab : a < b) : upperBounds (Ioo a b) = Ici b

Full source

theorem upperBounds_Ioo {a b : γ} (hab : a < b) : upperBounds (Ioo a b) = Ici b :=
  (isLUB_Ioo hab).upperBounds_eq

Upper Bounds of Open Interval: $\text{upperBounds}((a, b)) = [b, \infty)$

Informal description

For any elements $a$ and $b$ in a partially ordered type $\gamma$ with $a < b$, the set of upper bounds of the open interval $(a, b) = \{x \in \gamma \mid a < x < b\}$ is equal to the left-closed right-infinite interval $[b, \infty) = \{x \in \gamma \mid b \leq x\}$.

isLUB_Ico theorem

{a b : γ} (hab : a < b) : IsLUB (Ico a b) b

Full source

theorem isLUB_Ico {a b : γ} (hab : a < b) : IsLUB (Ico a b) b := by
  simpa only [Ioc_toDual] using isGLB_Ioc hab.dual

$b$ is the supremum of $[a, b)$ when $a < b$

Informal description

For any elements $a$ and $b$ in a partially ordered type $\gamma$ with $a < b$, the element $b$ is the least upper bound (supremum) of the left-closed right-open interval $[a, b) = \{x \in \gamma \mid a \leq x < b\}$.

upperBounds_Ico theorem

{a b : γ} (hab : a < b) : upperBounds (Ico a b) = Ici b

Full source

theorem upperBounds_Ico {a b : γ} (hab : a < b) : upperBounds (Ico a b) = Ici b :=
  (isLUB_Ico hab).upperBounds_eq

Upper Bounds of $[a, b)$: $\text{upperBounds}([a, b)) = [b, \infty)$

Informal description

For any elements $a$ and $b$ in a partially ordered type $\gamma$ with $a < b$, the set of upper bounds of the left-closed right-open interval $[a, b) = \{x \in \gamma \mid a \leq x < b\}$ is equal to the left-closed right-infinite interval $[b, \infty) = \{x \in \gamma \mid b \leq x\}$.

bddBelow_iff_subset_Ici theorem

: BddBelow s ↔ ∃ a, s ⊆ Ici a

Full source

theorem bddBelow_iff_subset_Ici : BddBelowBddBelow s ↔ ∃ a, s ⊆ Ici a :=
  Iff.rfl

Characterization of Bounded Below Sets via Interval Containment

Informal description

A set $s$ in a partially ordered type $\alpha$ is bounded below if and only if there exists an element $a \in \alpha$ such that $s$ is contained in the interval $[a, \infty)$ (i.e., $s \subseteq \{x \in \alpha \mid a \leq x\}$).

bddAbove_iff_subset_Iic theorem

: BddAbove s ↔ ∃ a, s ⊆ Iic a

Full source

theorem bddAbove_iff_subset_Iic : BddAboveBddAbove s ↔ ∃ a, s ⊆ Iic a :=
  Iff.rfl

Characterization of Bounded Above Sets via Interval Containment

Informal description

A set $s$ in a preorder $\alpha$ is bounded above if and only if there exists an element $a \in \alpha$ such that $s$ is contained in the left-infinite right-closed interval $(-\infty, a]$.

bddBelow_bddAbove_iff_subset_Icc theorem

: BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Icc a b

Full source

theorem bddBelow_bddAbove_iff_subset_Icc : BddBelowBddBelow s ∧ BddAbove sBddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Icc a b := by
  simp [Ici_inter_Iic.symm, subset_inter_iff, bddBelow_iff_subset_Ici,
    bddAbove_iff_subset_Iic, exists_and_left, exists_and_right]

Characterization of Bounded Sets via Interval Containment

Informal description

A set $s$ in a preorder $\alpha$ is both bounded below and bounded above if and only if there exist elements $a, b \in \alpha$ such that $s$ is contained in the closed interval $[a, b]$.

isGreatest_univ_iff theorem

: IsGreatest univ a ↔ IsTop a

Full source

@[simp] theorem isGreatest_univ_iff : IsGreatestIsGreatest univ a ↔ IsTop a := by
  simp [IsGreatest, mem_upperBounds, IsTop]

Greatest Element of Universal Set iff Top Element

Informal description

An element $a$ is the greatest element of the universal set (i.e., the entire type $\alpha$) if and only if $a$ is the top element of $\alpha$.

isGreatest_univ theorem

[OrderTop α] : IsGreatest (univ : Set α) ⊤

Full source

theorem isGreatest_univ [OrderTop α] : IsGreatest (univ : Set α) ⊤ :=
  isGreatest_univ_iff.2 isTop_top

Greatest element of universal set is top element

Informal description

In a partially ordered type $\alpha$ with a greatest element $\top$, the universal set (i.e., the entire type $\alpha$) has $\top$ as its greatest element.

OrderTop.upperBounds_univ theorem

[PartialOrder γ] [OrderTop γ] : upperBounds (univ : Set γ) = {⊤}

Full source

@[simp]
theorem OrderTop.upperBounds_univ [PartialOrder γ] [OrderTop γ] :
    upperBounds (univ : Set γ) = {⊤} := by rw [isGreatest_univ.upperBounds_eq, Ici_top]

Upper Bounds of Universal Set in Order with Top Element: $\text{upperBounds}(\text{univ}) = \{\top\}$

Informal description

In a partially ordered set $\gamma$ with a greatest element $\top$, the set of upper bounds of the universal set (i.e., the entire type $\gamma$) is the singleton set $\{\top\}$.

isLUB_univ theorem

[OrderTop α] : IsLUB (univ : Set α) ⊤

Full source

theorem isLUB_univ [OrderTop α] : IsLUB (univ : Set α) ⊤ :=
  isGreatest_univ.isLUB

Universal Set's Least Upper Bound is Top Element

Informal description

In a partially ordered type $\alpha$ with a greatest element $\top$, the universal set (i.e., the entire type $\alpha$) has $\top$ as its least upper bound (supremum).

OrderBot.lowerBounds_univ theorem

[PartialOrder γ] [OrderBot γ] : lowerBounds (univ : Set γ) = {⊥}

Full source

@[simp]
theorem OrderBot.lowerBounds_univ [PartialOrder γ] [OrderBot γ] :
    lowerBounds (univ : Set γ) = {⊥} :=
  @OrderTop.upperBounds_univ γᵒᵈ _ _

Lower Bounds of Universal Set in Order with Bottom Element: $\text{lowerBounds}(\text{univ}) = \{\bot\}$

Informal description

In a partially ordered set $\gamma$ with a least element $\bot$, the set of lower bounds of the universal set (i.e., the entire type $\gamma$) is the singleton set $\{\bot\}$.

isLeast_univ_iff theorem

: IsLeast univ a ↔ IsBot a

Full source

@[simp] theorem isLeast_univ_iff : IsLeastIsLeast univ a ↔ IsBot a :=
  @isGreatest_univ_iff αᵒᵈ _ _

Least Element of Universal Set iff Bottom Element

Informal description

An element $a$ is the least element of the universal set (i.e., the entire type $\alpha$) if and only if $a$ is the bottom element of $\alpha$.

isLeast_univ theorem

[OrderBot α] : IsLeast (univ : Set α) ⊥

Full source

theorem isLeast_univ [OrderBot α] : IsLeast (univ : Set α) ⊥ :=
  @isGreatest_univ αᵒᵈ _ _

Least element of universal set is bottom element

Informal description

In a partially ordered type $\alpha$ with a least element $\bot$, the universal set (i.e., the entire type $\alpha$) has $\bot$ as its least element.

isGLB_univ theorem

[OrderBot α] : IsGLB (univ : Set α) ⊥

Full source

theorem isGLB_univ [OrderBot α] : IsGLB (univ : Set α) ⊥ :=
  isLeast_univ.isGLB

Greatest Lower Bound of Universal Set is Bottom Element

Informal description

In a partially ordered type $\alpha$ with a least element $\bot$, the greatest lower bound (infimum) of the universal set (i.e., the entire type $\alpha$) is $\bot$.

NoTopOrder.upperBounds_univ theorem

[NoTopOrder α] : upperBounds (univ : Set α) = ∅

Full source

@[simp]
theorem NoTopOrder.upperBounds_univ [NoTopOrder α] : upperBounds (univ : Set α) = ∅ :=
  eq_empty_of_subset_empty fun b hb =>
    not_isTop b fun x => hb (mem_univ x)

Empty Upper Bounds for Universal Set in No-Top-Order Types

Informal description

In a type $\alpha$ with no top element (i.e., for every $x \in \alpha$, there exists $y \in \alpha$ such that $x < y$), the set of upper bounds of the universal set $\text{univ} = \alpha$ is empty.

NoBotOrder.lowerBounds_univ theorem

[NoBotOrder α] : lowerBounds (univ : Set α) = ∅

Full source

@[simp]
theorem NoBotOrder.lowerBounds_univ [NoBotOrder α] : lowerBounds (univ : Set α) = ∅ :=
  @NoTopOrder.upperBounds_univ αᵒᵈ _ _

Empty Lower Bounds for Universal Set in No-Bottom-Order Types

Informal description

In a type $\alpha$ with no bottom element (i.e., for every $x \in \alpha$, there exists $y \in \alpha$ such that $y < x$), the set of lower bounds of the universal set $\text{univ} = \alpha$ is empty.

not_bddAbove_univ theorem

[NoTopOrder α] : ¬BddAbove (univ : Set α)

Full source

@[simp]
theorem not_bddAbove_univ [NoTopOrder α] : ¬BddAbove (univ : Set α) := by simp [BddAbove]

Universal Set is Unbounded Above in No-Top-Order Types

Informal description

In a type $\alpha$ with no top element (i.e., for every $x \in \alpha$, there exists $y \in \alpha$ such that $x < y$), the universal set $\text{univ} = \alpha$ is not bounded above.

not_bddBelow_univ theorem

[NoBotOrder α] : ¬BddBelow (univ : Set α)

Full source

@[simp]
theorem not_bddBelow_univ [NoBotOrder α] : ¬BddBelow (univ : Set α) :=
  @not_bddAbove_univ αᵒᵈ _ _

Universal set is unbounded below in no-bottom-order types

Informal description

In a type $\alpha$ with no bottom element (i.e., for every $x \in \alpha$, there exists $y \in \alpha$ such that $y < x$), the universal set $\alpha$ is not bounded below.

upperBounds_empty theorem

: upperBounds (∅ : Set α) = univ

Full source

@[simp]
theorem upperBounds_empty : upperBounds (∅ : Set α) = univ := by
  simp only [upperBounds, eq_univ_iff_forall, mem_setOf_eq, forall_mem_empty, forall_true_iff]

Upper Bounds of Empty Set are Universal Set

Informal description

For any type $\alpha$ with a preorder, the set of upper bounds of the empty set $\emptyset$ is equal to the universal set $\text{univ}$ (the set of all elements of $\alpha$).

lowerBounds_empty theorem

: lowerBounds (∅ : Set α) = univ

Full source

@[simp]
theorem lowerBounds_empty : lowerBounds (∅ : Set α) = univ :=
  @upperBounds_empty αᵒᵈ _

Lower Bounds of Empty Set are Universal Set

Informal description

For any type $\alpha$ with a preorder, the set of lower bounds of the empty set $\emptyset$ is equal to the universal set $\text{univ}$ (the set of all elements of $\alpha$).

bddAbove_empty theorem

[Nonempty α] : BddAbove (∅ : Set α)

Full source

@[simp]
theorem bddAbove_empty [Nonempty α] : BddAbove (∅ : Set α) := by
  simp only [BddAbove, upperBounds_empty, univ_nonempty]

Empty Set is Bounded Above in Nonempty Preorder

Informal description

In any nonempty type $\alpha$ with a preorder, the empty set is bounded above.

bddBelow_empty theorem

[Nonempty α] : BddBelow (∅ : Set α)

Full source

@[simp]
theorem bddBelow_empty [Nonempty α] : BddBelow (∅ : Set α) := by
  simp only [BddBelow, lowerBounds_empty, univ_nonempty]

Empty Set is Bounded Below in Nonempty Preorder

Informal description

In any nonempty type $\alpha$ with a preorder, the empty set is bounded below.

isGLB_empty_iff theorem

: IsGLB ∅ a ↔ IsTop a

Full source

@[simp] theorem isGLB_empty_iff : IsGLBIsGLB ∅ a ↔ IsTop a := by
  simp [IsGLB]

Greatest Lower Bound of Empty Set is Top Element

Informal description

An element $a$ in a partially ordered type $\alpha$ is the greatest lower bound of the empty set if and only if $a$ is the top element of $\alpha$ (i.e., $x \leq a$ for all $x \in \alpha$).

isLUB_empty_iff theorem

: IsLUB ∅ a ↔ IsBot a

Full source

@[simp] theorem isLUB_empty_iff : IsLUBIsLUB ∅ a ↔ IsBot a :=
  @isGLB_empty_iff αᵒᵈ _ _

Least Upper Bound of Empty Set is Bottom Element

Informal description

An element $a$ in a partially ordered type $\alpha$ is the least upper bound of the empty set if and only if $a$ is the bottom element of $\alpha$ (i.e., $a \leq x$ for all $x \in \alpha$).

isGLB_empty theorem

[OrderTop α] : IsGLB ∅ (⊤ : α)

Full source

theorem isGLB_empty [OrderTop α] : IsGLB ∅ (⊤ : α) :=
  isGLB_empty_iff.2 isTop_top

Greatest lower bound of empty set is top element

Informal description

In a partially ordered type $\alpha$ with a greatest element $\top$, the empty set $\emptyset$ has $\top$ as its greatest lower bound.

isLUB_empty theorem

[OrderBot α] : IsLUB ∅ (⊥ : α)

Full source

theorem isLUB_empty [OrderBot α] : IsLUB ∅ (⊥ : α) :=
  @isGLB_empty αᵒᵈ _ _

Least upper bound of empty set is bottom element

Informal description

In a partially ordered type $\alpha$ with a bottom element $\bot$, the empty set $\emptyset$ has $\bot$ as its least upper bound.

IsLUB.nonempty theorem

[NoBotOrder α] (hs : IsLUB s a) : s.Nonempty

Full source

theorem IsLUB.nonempty [NoBotOrder α] (hs : IsLUB s a) : s.Nonempty :=
  nonempty_iff_ne_empty.2 fun h =>
    not_isBot a fun _ => hs.right <| by rw [h, upperBounds_empty]; exact mem_univ _

Nonemptiness of Set with Least Upper Bound in No-Bottom-Order

Informal description

Let $\alpha$ be a partially ordered type with no bottom element (i.e., for every $x \in \alpha$, there exists $y \in \alpha$ such that $y < x$). If $a$ is the least upper bound of a set $s \subseteq \alpha$, then $s$ is nonempty.

IsGLB.nonempty theorem

[NoTopOrder α] (hs : IsGLB s a) : s.Nonempty

Full source

theorem IsGLB.nonempty [NoTopOrder α] (hs : IsGLB s a) : s.Nonempty :=
  hs.dual.nonempty

Nonemptiness of Set with Greatest Lower Bound in No-Top-Order

Informal description

Let $\alpha$ be a partially ordered type with no top element (i.e., for every $x \in \alpha$, there exists $y \in \alpha$ such that $x < y$). If $a$ is the greatest lower bound of a set $s \subseteq \alpha$, then $s$ is nonempty.

nonempty_of_not_bddAbove theorem

[ha : Nonempty α] (h : ¬BddAbove s) : s.Nonempty

Full source

theorem nonempty_of_not_bddAbove [ha : Nonempty α] (h : ¬BddAbove s) : s.Nonempty :=
  (Nonempty.elim ha) fun x => (not_bddAbove_iff'.1 h x).imp fun _ ha => ha.1

Nonemptiness of Unbounded Above Sets in Nonempty Preorders

Informal description

Let $\alpha$ be a nonempty type with a preorder. If a set $s \subseteq \alpha$ is not bounded above, then $s$ is nonempty.

nonempty_of_not_bddBelow theorem

[Nonempty α] (h : ¬BddBelow s) : s.Nonempty

Full source

theorem nonempty_of_not_bddBelow [Nonempty α] (h : ¬BddBelow s) : s.Nonempty :=
  @nonempty_of_not_bddAbove αᵒᵈ _ _ _ h

Nonemptiness of Unbounded Below Sets in Nonempty Preorders

Informal description

Let $\alpha$ be a nonempty type with a preorder. If a set $s \subseteq \alpha$ is not bounded below, then $s$ is nonempty.

bddAbove_insert theorem

[IsDirected α (· ≤ ·)] {s : Set α} {a : α} : BddAbove (insert a s) ↔ BddAbove s

Full source

/-- Adding a point to a set preserves its boundedness above. -/
@[simp]
theorem bddAbove_insert [IsDirected α (· ≤ ·)] {s : Set α} {a : α} :
    BddAboveBddAbove (insert a s) ↔ BddAbove s := by
  simp only [insert_eq, bddAbove_union, bddAbove_singleton, true_and]

Insertion Preserves Boundedness Above in Directed Orders

Informal description

Let $\alpha$ be a type with a directed order relation $\leq$. For any set $s \subseteq \alpha$ and any element $a \in \alpha$, the set $\{a\} \cup s$ is bounded above if and only if $s$ is bounded above.

BddAbove.insert theorem

[IsDirected α (· ≤ ·)] {s : Set α} (a : α) : BddAbove s → BddAbove (insert a s)

Full source

protected theorem BddAbove.insert [IsDirected α (· ≤ ·)] {s : Set α} (a : α) :
    BddAbove s → BddAbove (insert a s) :=
  bddAbove_insert.2

Insertion Preserves Upper Boundedness in Directed Orders

Informal description

Let $\alpha$ be a type with a directed order relation $\leq$. For any set $s \subseteq \alpha$ and any element $a \in \alpha$, if $s$ is bounded above, then the set $\{a\} \cup s$ is also bounded above.

bddBelow_insert theorem

[IsDirected α (· ≥ ·)] {s : Set α} {a : α} : BddBelow (insert a s) ↔ BddBelow s

Full source

/-- Adding a point to a set preserves its boundedness below. -/
@[simp]
theorem bddBelow_insert [IsDirected α (· ≥ ·)] {s : Set α} {a : α} :
    BddBelowBddBelow (insert a s) ↔ BddBelow s := by
  simp only [insert_eq, bddBelow_union, bddBelow_singleton, true_and]

Insertion Preserves Boundedness Below in Directed Orders

Informal description

Let $\alpha$ be a type with a directed order relation $\geq$. For any set $s \subseteq \alpha$ and any element $a \in \alpha$, the set $\{a\} \cup s$ is bounded below if and only if $s$ is bounded below.

BddBelow.insert theorem

[IsDirected α (· ≥ ·)] {s : Set α} (a : α) : BddBelow s → BddBelow (insert a s)

Full source

protected theorem BddBelow.insert [IsDirected α (· ≥ ·)] {s : Set α} (a : α) :
    BddBelow s → BddBelow (insert a s) :=
  bddBelow_insert.2

Insertion Preserves Lower Boundedness in Directed Orders

Informal description

Let $\alpha$ be a type with a directed order relation $\geq$. For any set $s \subseteq \alpha$ and any element $a \in \alpha$, if $s$ is bounded below, then the set $\{a\} \cup s$ is also bounded below.

IsLUB.insert theorem

[SemilatticeSup γ] (a) {b} {s : Set γ} (hs : IsLUB s b) : IsLUB (insert a s) (a ⊔ b)

Full source

protected theorem IsLUB.insert [SemilatticeSup γ] (a) {b} {s : Set γ} (hs : IsLUB s b) :
    IsLUB (insert a s) (a ⊔ b) := by
  rw [insert_eq]
  exact isLUB_singleton.union hs

Supremum of Inserted Set in Semilattices

Informal description

Let $\gamma$ be a type with a semilattice structure under the supremum operation $\sqcup$. For any element $a \in \gamma$, any set $s \subseteq \gamma$, and any element $b \in \gamma$, if $b$ is the least upper bound of $s$, then $a \sqcup b$ is the least upper bound of the set $\{a\} \cup s$.

IsGLB.insert theorem

[SemilatticeInf γ] (a) {b} {s : Set γ} (hs : IsGLB s b) : IsGLB (insert a s) (a ⊓ b)

Full source

protected theorem IsGLB.insert [SemilatticeInf γ] (a) {b} {s : Set γ} (hs : IsGLB s b) :
    IsGLB (insert a s) (a ⊓ b) := by
  rw [insert_eq]
  exact isGLB_singleton.union hs

Infimum of Insertion in Semilattices

Informal description

Let $\gamma$ be a type with a semilattice structure under the infimum operation $\sqcap$. For any set $s \subseteq \gamma$ and elements $a, b \in \gamma$, if $b$ is the greatest lower bound of $s$, then $a \sqcap b$ is the greatest lower bound of the set $\{a\} \cup s$.

IsGreatest.insert theorem

[LinearOrder γ] (a) {b} {s : Set γ} (hs : IsGreatest s b) : IsGreatest (insert a s) (max a b)

Full source

protected theorem IsGreatest.insert [LinearOrder γ] (a) {b} {s : Set γ} (hs : IsGreatest s b) :
    IsGreatest (insert a s) (max a b) := by
  rw [insert_eq]
  exact isGreatest_singleton.union hs

Greatest element of inserted set is the maximum

Informal description

Let $\gamma$ be a linearly ordered set, $a \in \gamma$, and $s \subseteq \gamma$ a subset with greatest element $b$. Then the greatest element of the set $\{a\} \cup s$ is $\max(a, b)$.

IsLeast.insert theorem

[LinearOrder γ] (a) {b} {s : Set γ} (hs : IsLeast s b) : IsLeast (insert a s) (min a b)

Full source

protected theorem IsLeast.insert [LinearOrder γ] (a) {b} {s : Set γ} (hs : IsLeast s b) :
    IsLeast (insert a s) (min a b) := by
  rw [insert_eq]
  exact isLeast_singleton.union hs

Least Element of Inserted Set is Minimum in Linear Order

Informal description

Let $\gamma$ be a linearly ordered set, $a \in \gamma$, and $s \subseteq \gamma$ a subset with least element $b$. Then the least element of the set $\{a\} \cup s$ is $\min(a, b)$.

upperBounds_insert theorem

(a : α) (s : Set α) : upperBounds (insert a s) = Ici a ∩ upperBounds s

Full source

@[simp]
theorem upperBounds_insert (a : α) (s : Set α) :
    upperBounds (insert a s) = IciIci a ∩ upperBounds s := by
  rw [insert_eq, upperBounds_union, upperBounds_singleton]

Upper Bounds of Inserted Set: $\text{upperBounds}(\{a\} \cup s) = [a, \infty) \cap \text{upperBounds}(s)$

Informal description

For any element $a$ in a preordered type $\alpha$ and any subset $s \subseteq \alpha$, the set of upper bounds of $\{a\} \cup s$ is equal to the intersection of the interval $[a, \infty)$ and the upper bounds of $s$, i.e., \[ \text{upperBounds}(\{a\} \cup s) = [a, \infty) \cap \text{upperBounds}(s). \]

lowerBounds_insert theorem

(a : α) (s : Set α) : lowerBounds (insert a s) = Iic a ∩ lowerBounds s

Full source

@[simp]
theorem lowerBounds_insert (a : α) (s : Set α) :
    lowerBounds (insert a s) = IicIic a ∩ lowerBounds s := by
  rw [insert_eq, lowerBounds_union, lowerBounds_singleton]

Lower Bounds of Inserted Set: $\text{lowerBounds}(\{a\} \cup s) = (-\infty, a] \cap \text{lowerBounds}(s)$

Informal description

For any element $a$ in a preorder $\alpha$ and any subset $s \subseteq \alpha$, the set of lower bounds of the set $\{a\} \cup s$ is equal to the intersection of the left-infinite right-closed interval $(-\infty, a]$ and the set of lower bounds of $s$, i.e., \[ \text{lowerBounds}(\{a\} \cup s) = (-\infty, a] \cap \text{lowerBounds}(s). \]

OrderTop.bddAbove theorem

[OrderTop α] (s : Set α) : BddAbove s

Full source

/-- When there is a global maximum, every set is bounded above. -/
@[simp]
protected theorem OrderTop.bddAbove [OrderTop α] (s : Set α) : BddAbove s :=
  ⟨⊤, fun a _ => OrderTop.le_top a⟩

Every set is bounded above in an order with top element

Informal description

In a partially ordered set $\alpha$ with a greatest element $\top$, every subset $s \subseteq \alpha$ is bounded above. That is, there exists an element $x \in \alpha$ such that $a \leq x$ for all $a \in s$.

OrderBot.bddBelow theorem

[OrderBot α] (s : Set α) : BddBelow s

Full source

/-- When there is a global minimum, every set is bounded below. -/
@[simp]
protected theorem OrderBot.bddBelow [OrderBot α] (s : Set α) : BddBelow s :=
  ⟨⊥, fun a _ => OrderBot.bot_le a⟩

Every set is bounded below in an order with bottom element

Informal description

In a partially ordered set $\alpha$ with a least element $\bot$, every subset $s \subseteq \alpha$ is bounded below. That is, there exists an element $x \in \alpha$ such that $x \leq a$ for all $a \in s$.

tacticBddDefault definition

: Lean.ParserDescr✝

Full source

macromacro "bddDefault" : tactic =>
  `(tactic| first
    | apply OrderTop.bddAbove
    | apply OrderBot.bddBelow)

Default boundedness tactic for complete lattices

Informal description

The tactic `bddDefault` automatically fills in boundedness proofs for sets in complete lattices. It first attempts to apply `OrderTop.bddAbove` to prove boundedness above, and if that fails, it applies `OrderBot.bddBelow` to prove boundedness below.

isLUB_pair theorem

[SemilatticeSup γ] {a b : γ} : IsLUB { a, b } (a ⊔ b)

Full source

theorem isLUB_pair [SemilatticeSup γ] {a b : γ} : IsLUB {a, b} (a ⊔ b) :=
  isLUB_singleton.insert _

Supremum of a Pair in a Semilattice

Informal description

Let $\gamma$ be a type with a semilattice structure under the supremum operation $\sqcup$. For any two elements $a, b \in \gamma$, the least upper bound of the set $\{a, b\}$ is $a \sqcup b$.

isGLB_pair theorem

[SemilatticeInf γ] {a b : γ} : IsGLB { a, b } (a ⊓ b)

Full source

theorem isGLB_pair [SemilatticeInf γ] {a b : γ} : IsGLB {a, b} (a ⊓ b) :=
  isGLB_singleton.insert _

Infimum is Greatest Lower Bound of a Pair in a Semilattice

Informal description

Let $\gamma$ be a type with a semilattice structure under the infimum operation $\sqcap$. For any two elements $a, b \in \gamma$, the infimum $a \sqcap b$ is the greatest lower bound of the set $\{a, b\}$.

isLeast_pair theorem

[LinearOrder γ] {a b : γ} : IsLeast { a, b } (min a b)

Full source

theorem isLeast_pair [LinearOrder γ] {a b : γ} : IsLeast {a, b} (min a b) :=
  isLeast_singleton.insert _

Least element of a pair is their minimum

Informal description

Let $\gamma$ be a linearly ordered set and $a, b \in \gamma$. Then the least element of the two-element set $\{a, b\}$ is $\min(a, b)$.

isGreatest_pair theorem

[LinearOrder γ] {a b : γ} : IsGreatest { a, b } (max a b)

Full source

theorem isGreatest_pair [LinearOrder γ] {a b : γ} : IsGreatest {a, b} (max a b) :=
  isGreatest_singleton.insert _

Greatest element of a pair is their maximum

Informal description

Let $\gamma$ be a linearly ordered set and $a, b \in \gamma$. Then the greatest element of the two-element set $\{a, b\}$ is $\max(a, b)$.

isLUB_lowerBounds theorem

: IsLUB (lowerBounds s) a ↔ IsGLB s a

Full source

@[simp]
theorem isLUB_lowerBounds : IsLUBIsLUB (lowerBounds s) a ↔ IsGLB s a :=
  ⟨fun H => ⟨fun _ hx => H.2 <| subset_upperBounds_lowerBounds s hx, H.1⟩, IsGreatest.isLUB⟩

Least Upper Bound of Lower Bounds is Greatest Lower Bound

Informal description

For any subset $s$ of a partially ordered set $\alpha$, an element $a$ is the least upper bound of the set of lower bounds of $s$ if and only if $a$ is the greatest lower bound of $s$.

isGLB_upperBounds theorem

: IsGLB (upperBounds s) a ↔ IsLUB s a

Full source

@[simp]
theorem isGLB_upperBounds : IsGLBIsGLB (upperBounds s) a ↔ IsLUB s a :=
  @isLUB_lowerBounds αᵒᵈ _ _ _

Greatest Lower Bound of Upper Bounds is Least Upper Bound

Informal description

For any subset $s$ of a partially ordered set $\alpha$, an element $a$ is the greatest lower bound of the set of upper bounds of $s$ if and only if $a$ is the least upper bound of $s$.

lowerBounds_le_upperBounds theorem

(ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds s) : s.Nonempty → a ≤ b

Full source

theorem lowerBounds_le_upperBounds (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds s) :
    s.Nonempty → a ≤ b
  | ⟨_, hc⟩ => le_trans (ha hc) (hb hc)

Lower Bound Does Not Exceed Upper Bound for Nonempty Sets

Informal description

For any elements $a$ and $b$ in a partially ordered set $\alpha$, if $a$ is a lower bound of a nonempty set $s \subseteq \alpha$ and $b$ is an upper bound of $s$, then $a \leq b$.

isGLB_le_isLUB theorem

(ha : IsGLB s a) (hb : IsLUB s b) (hs : s.Nonempty) : a ≤ b

Full source

theorem isGLB_le_isLUB (ha : IsGLB s a) (hb : IsLUB s b) (hs : s.Nonempty) : a ≤ b :=
  lowerBounds_le_upperBounds ha.1 hb.1 hs

Greatest Lower Bound Does Not Exceed Least Upper Bound for Nonempty Sets

Informal description

For any nonempty set $s$ in a partially ordered type $\alpha$, if $a$ is the greatest lower bound of $s$ and $b$ is the least upper bound of $s$, then $a \leq b$.

isLUB_lt_iff theorem

(ha : IsLUB s a) : a < b ↔ ∃ c ∈ upperBounds s, c < b

Full source

theorem isLUB_lt_iff (ha : IsLUB s a) : a < b ↔ ∃ c ∈ upperBounds s, c < b :=
  ⟨fun hb => ⟨a, ha.1, hb⟩, fun ⟨_, hcs, hcb⟩ => lt_of_le_of_lt (ha.2 hcs) hcb⟩

Characterization of Least Upper Bound Being Less Than Another Element

Informal description

Let $s$ be a set in a partially ordered type $\alpha$, and let $a$ be the least upper bound of $s$. Then $a < b$ if and only if there exists an element $c$ in the set of upper bounds of $s$ such that $c < b$.

lt_isGLB_iff theorem

(ha : IsGLB s a) : b < a ↔ ∃ c ∈ lowerBounds s, b < c

Full source

theorem lt_isGLB_iff (ha : IsGLB s a) : b < a ↔ ∃ c ∈ lowerBounds s, b < c :=
  isLUB_lt_iff ha.dual

Characterization of Elements Below Greatest Lower Bound via Lower Bounds

Informal description

Let $s$ be a set in a partially ordered type $\alpha$, and let $a$ be the greatest lower bound of $s$. Then $b < a$ if and only if there exists an element $c$ in the set of lower bounds of $s$ such that $b < c$.

le_of_isLUB_le_isGLB theorem

{x y} (ha : IsGLB s a) (hb : IsLUB s b) (hab : b ≤ a) (hx : x ∈ s) (hy : y ∈ s) : x ≤ y

Full source

theorem le_of_isLUB_le_isGLB {x y} (ha : IsGLB s a) (hb : IsLUB s b) (hab : b ≤ a) (hx : x ∈ s)
    (hy : y ∈ s) : x ≤ y :=
  calc
    x ≤ b := hb.1 hx
    _ ≤ a := hab
    _ ≤ y := ha.1 hy

Ordering Relation between Elements of a Set with Bounded Infimum and Supremum

Informal description

Let $s$ be a set in a partially ordered type $\alpha$, with $a$ as its greatest lower bound and $b$ as its least upper bound. If $b \leq a$, then for any elements $x, y \in s$, we have $x \leq y$.

IsLeast.unique theorem

(Ha : IsLeast s a) (Hb : IsLeast s b) : a = b

Full source

theorem IsLeast.unique (Ha : IsLeast s a) (Hb : IsLeast s b) : a = b :=
  le_antisymm (Ha.right Hb.left) (Hb.right Ha.left)

Uniqueness of Least Element in a Partially Ordered Set

Informal description

If $a$ and $b$ are both least elements of a set $s$ in a partially ordered type $\alpha$, then $a = b$.

IsLeast.isLeast_iff_eq theorem

(Ha : IsLeast s a) : IsLeast s b ↔ a = b

Full source

theorem IsLeast.isLeast_iff_eq (Ha : IsLeast s a) : IsLeastIsLeast s b ↔ a = b :=
  Iff.intro Ha.unique fun h => h ▸ Ha

Characterization of Least Elements via Equality

Informal description

Given a partially ordered set $\alpha$ and a subset $s \subseteq \alpha$, if $a$ is a least element of $s$, then for any element $b$, $b$ is a least element of $s$ if and only if $b = a$.

IsGreatest.unique theorem

(Ha : IsGreatest s a) (Hb : IsGreatest s b) : a = b

Full source

theorem IsGreatest.unique (Ha : IsGreatest s a) (Hb : IsGreatest s b) : a = b :=
  le_antisymm (Hb.right Ha.left) (Ha.right Hb.left)

Uniqueness of Greatest Element in a Partially Ordered Set

Informal description

If $a$ and $b$ are both greatest elements of a set $s$ in a partially ordered type $\alpha$, then $a = b$.

IsGreatest.isGreatest_iff_eq theorem

(Ha : IsGreatest s a) : IsGreatest s b ↔ a = b

Full source

theorem IsGreatest.isGreatest_iff_eq (Ha : IsGreatest s a) : IsGreatestIsGreatest s b ↔ a = b :=
  Iff.intro Ha.unique fun h => h ▸ Ha

Characterization of Greatest Elements via Equality

Informal description

Given a partially ordered set $\alpha$ and a subset $s \subseteq \alpha$, if $a$ is the greatest element of $s$, then for any element $b$, $b$ is the greatest element of $s$ if and only if $b = a$.

IsLUB.unique theorem

(Ha : IsLUB s a) (Hb : IsLUB s b) : a = b

Full source

theorem IsLUB.unique (Ha : IsLUB s a) (Hb : IsLUB s b) : a = b :=
  IsLeast.unique Ha Hb

Uniqueness of Least Upper Bound (Supremum)

Informal description

If $a$ and $b$ are both least upper bounds (suprema) of a set $s$ in a partially ordered type $\alpha$, then $a = b$.

IsGLB.unique theorem

(Ha : IsGLB s a) (Hb : IsGLB s b) : a = b

Full source

theorem IsGLB.unique (Ha : IsGLB s a) (Hb : IsGLB s b) : a = b :=
  IsGreatest.unique Ha Hb

Uniqueness of Greatest Lower Bound

Informal description

If $a$ and $b$ are both greatest lower bounds of a set $s$ in a partially ordered type $\alpha$, then $a = b$.

Set.subsingleton_of_isLUB_le_isGLB theorem

(Ha : IsGLB s a) (Hb : IsLUB s b) (hab : b ≤ a) : s.Subsingleton

Full source

theorem Set.subsingleton_of_isLUB_le_isGLB (Ha : IsGLB s a) (Hb : IsLUB s b) (hab : b ≤ a) :
    s.Subsingleton := fun _ hx _ hy =>
  le_antisymm (le_of_isLUB_le_isGLB Ha Hb hab hx hy) (le_of_isLUB_le_isGLB Ha Hb hab hy hx)

Subsingleton condition for sets with ordered bounds

Informal description

Let $s$ be a set in a partially ordered type $\alpha$, with $a$ as its greatest lower bound and $b$ as its least upper bound. If $b \leq a$, then $s$ contains at most one element (i.e., $s$ is a subsingleton).

isGLB_lt_isLUB_of_ne theorem

(Ha : IsGLB s a) (Hb : IsLUB s b) {x y} (Hx : x ∈ s) (Hy : y ∈ s) (Hxy : x ≠ y) : a < b

Full source

theorem isGLB_lt_isLUB_of_ne (Ha : IsGLB s a) (Hb : IsLUB s b) {x y} (Hx : x ∈ s) (Hy : y ∈ s)
    (Hxy : x ≠ y) : a < b :=
  lt_iff_le_not_le.2
    ⟨lowerBounds_le_upperBounds Ha.1 Hb.1 ⟨x, Hx⟩, fun hab =>
      Hxy <| Set.subsingleton_of_isLUB_le_isGLB Ha Hb hab Hx Hy⟩

Strict Inequality Between Bounds for Non-Singleton Sets

Informal description

Let $s$ be a set in a partially ordered type $\alpha$, with $a$ as its greatest lower bound and $b$ as its least upper bound. If there exist distinct elements $x, y \in s$, then $a < b$.

lt_isLUB_iff theorem

(h : IsLUB s a) : b < a ↔ ∃ c ∈ s, b < c

Full source

theorem lt_isLUB_iff (h : IsLUB s a) : b < a ↔ ∃ c ∈ s, b < c := by
  simp_rw [← not_le, isLUB_le_iff h, mem_upperBounds, not_forall, not_le, exists_prop]

Characterization of elements strictly below the supremum: $b < \sup s \leftrightarrow \exists c \in s, b < c$

Informal description

Let $s$ be a subset of a partially ordered set $\alpha$, and let $a$ be the least upper bound of $s$. For any element $b \in \alpha$, we have $b < a$ if and only if there exists an element $c \in s$ such that $b < c$.

isGLB_lt_iff theorem

(h : IsGLB s a) : a < b ↔ ∃ c ∈ s, c < b

Full source

theorem isGLB_lt_iff (h : IsGLB s a) : a < b ↔ ∃ c ∈ s, c < b :=
  lt_isLUB_iff h.dual

Characterization of elements strictly above the infimum: $a < b \leftrightarrow \exists c \in s, c < b$

Informal description

Let $s$ be a subset of a partially ordered set $\alpha$, and let $a$ be the greatest lower bound of $s$. For any element $b \in \alpha$, we have $a < b$ if and only if there exists an element $c \in s$ such that $c < b$.

IsLUB.exists_between theorem

(h : IsLUB s a) (hb : b < a) : ∃ c ∈ s, b < c ∧ c ≤ a

Full source

theorem IsLUB.exists_between (h : IsLUB s a) (hb : b < a) : ∃ c ∈ s, b < c ∧ c ≤ a :=
  let ⟨c, hcs, hbc⟩ := (lt_isLUB_iff h).1 hb
  ⟨c, hcs, hbc, h.1 hcs⟩

Existence of Intermediate Element Below Supremum

Informal description

Let $s$ be a subset of a partially ordered set $\alpha$, and let $a$ be the least upper bound of $s$. For any element $b \in \alpha$ such that $b < a$, there exists an element $c \in s$ satisfying $b < c \leq a$.

IsLUB.exists_between' theorem

(h : IsLUB s a) (h' : a ∉ s) (hb : b < a) : ∃ c ∈ s, b < c ∧ c < a

Full source

theorem IsLUB.exists_between' (h : IsLUB s a) (h' : a ∉ s) (hb : b < a) : ∃ c ∈ s, b < c ∧ c < a :=
  let ⟨c, hcs, hbc, hca⟩ := h.exists_between hb
  ⟨c, hcs, hbc, hca.lt_of_ne fun hac => h' <| hac ▸ hcs⟩

Existence of Intermediate Element Strictly Below Supremum When Supremum Not in Set

Informal description

Let $s$ be a subset of a partially ordered set $\alpha$, and let $a$ be the least upper bound of $s$ with $a \notin s$. For any element $b \in \alpha$ such that $b < a$, there exists an element $c \in s$ satisfying $b < c < a$.

IsGLB.exists_between theorem

(h : IsGLB s a) (hb : a < b) : ∃ c ∈ s, a ≤ c ∧ c < b

Full source

theorem IsGLB.exists_between (h : IsGLB s a) (hb : a < b) : ∃ c ∈ s, a ≤ c ∧ c < b :=
  let ⟨c, hcs, hbc⟩ := (isGLB_lt_iff h).1 hb
  ⟨c, hcs, h.1 hcs, hbc⟩

Existence of Intermediate Element Above Infimum

Informal description

Let $s$ be a subset of a partially ordered set $\alpha$, and let $a$ be the greatest lower bound of $s$. For any element $b \in \alpha$ such that $a < b$, there exists an element $c \in s$ satisfying $a \leq c < b$.

IsGLB.exists_between' theorem

(h : IsGLB s a) (h' : a ∉ s) (hb : a < b) : ∃ c ∈ s, a < c ∧ c < b

Full source

theorem IsGLB.exists_between' (h : IsGLB s a) (h' : a ∉ s) (hb : a < b) : ∃ c ∈ s, a < c ∧ c < b :=
  let ⟨c, hcs, hac, hcb⟩ := h.exists_between hb
  ⟨c, hcs, hac.lt_of_ne fun hac => h' <| hac.symm ▸ hcs, hcb⟩

Existence of Intermediate Element Strictly Above Infimum When Infimum Not in Set

Informal description

Let $s$ be a subset of a partially ordered set $\alpha$, and let $a$ be the greatest lower bound of $s$ with $a \notin s$. For any element $b \in \alpha$ such that $a < b$, there exists an element $c \in s$ satisfying $a < c < b$.

isGreatest_himp theorem

[GeneralizedHeytingAlgebra α] (a b : α) : IsGreatest {w | w ⊓ a ≤ b} (a ⇨ b)

Full source

theorem isGreatest_himp [GeneralizedHeytingAlgebra α] (a b : α) :
    IsGreatest {w | w ⊓ a ≤ b} (a ⇨ b) := by
  simp [IsGreatest, mem_upperBounds]

Greatest Element Characterization of Heyting Implication: $a \Rightarrow b$ is the maximal solution to $w \sqcap a \leq b$

Informal description

In a generalized Heyting algebra $\alpha$, for any elements $a$ and $b$, the Heyting implication $a \Rightarrow b$ is the greatest element in the set $\{w \in \alpha \mid w \sqcap a \leq b\}$.

isLeast_sdiff theorem

[GeneralizedCoheytingAlgebra α] (a b : α) : IsLeast {w | a ≤ b ⊔ w} (a \ b)

Full source

theorem isLeast_sdiff [GeneralizedCoheytingAlgebra α] (a b : α) :
    IsLeast {w | a ≤ b ⊔ w} (a \ b) := by
  simp [IsLeast, mem_lowerBounds]

Least Element Characterization of Difference in Co-Heyting Algebras: $a \setminus b$ is the minimal solution to $a \leq b \sqcup w$

Informal description

In a generalized co-Heyting algebra $\alpha$, for any elements $a$ and $b$, the difference $a \setminus b$ is the least element in the set $\{w \in \alpha \mid a \leq b \sqcup w\}$.

isGreatest_compl theorem

[HeytingAlgebra α] (a : α) : IsGreatest {w | Disjoint w a} (aᶜ)

Full source

theorem isGreatest_compl [HeytingAlgebra α] (a : α) :
    IsGreatest {w | Disjoint w a} (aᶜ) := by
  simpa only [himp_bot, disjoint_iff_inf_le] using isGreatest_himp a ⊥

Pseudo-complement as Greatest Disjoint Element in Heyting Algebra

Informal description

In a Heyting algebra $\alpha$, for any element $a \in \alpha$, the pseudo-complement $\neg a$ is the greatest element in the set $\{w \in \alpha \mid w \sqcap a = \bot\}$.

isLeast_hnot theorem

[CoheytingAlgebra α] (a : α) : IsLeast {w | Codisjoint a w} (￢a)

Full source

theorem isLeast_hnot [CoheytingAlgebra α] (a : α) :
    IsLeast {w | Codisjoint a w} (￢a) := by
  simpa only [CoheytingAlgebra.top_sdiff, codisjoint_iff_le_sup] using isLeast_sdiff ⊤ a

Negation as Least Codisjoint Element in Co-Heyting Algebra

Informal description

In a co-Heyting algebra $\alpha$, for any element $a \in \alpha$, the negation $\neg a$ is the least element in the set $\{w \in \alpha \mid \text{Codisjoint}(a, w)\}$, where $\text{Codisjoint}(a, w)$ means $a \sqcup w = \top$.

Unbounded intervals