Upper / lower bounds

In this file we prove various lemmas about upper/lower bounds of a set: monotonicity, behaviour under ∪, ∩, insert, and provide formulas for ∅, univ, and intervals.

theorem mem_upperBounds {α : Type u_1} [Preorder α] {s : Set α} {a : α} : a ∈ upperBounds s ↔ ∀ x ∈ s, x ≤ a

theorem mem_lowerBounds {α : Type u_1} [Preorder α] {s : Set α} {a : α} : a ∈ lowerBounds s ↔ ∀ x ∈ s, a ≤ x

theorem mem_upperBounds_iff_subset_Iic {α : Type u_1} [Preorder α] {s : Set α} {a : α} : a ∈ upperBounds s ↔ s ⊆ Set.Iic a

theorem mem_lowerBounds_iff_subset_Ici {α : Type u_1} [Preorder α] {s : Set α} {a : α} : a ∈ lowerBounds s ↔ s ⊆ Set.Ici a

theorem bddAbove_def {α : Type u_1} [Preorder α] {s : Set α} : BddAbove s ↔ ∃ (x : α), ∀ y ∈ s, y ≤ x

theorem bddBelow_def {α : Type u_1} [Preorder α] {s : Set α} : BddBelow s ↔ ∃ (x : α), ∀ y ∈ s, x ≤ y

@[simp]

theorem Set.bounded_le {α : Type u_1} [Preorder α] {s : Set α} : Bounded LE.le s ↔ BddAbove s

@[simp]

theorem Set.bounded_ge {α : Type u_1} [Preorder α] {s : Set α} : Bounded (fun (a a_1 : α) => a_1 ≤ a) s ↔ BddBelow s

theorem top_mem_upperBounds {α : Type u_1} [Preorder α] [OrderTop α] (s : Set α) : ⊤ ∈ upperBounds s

theorem bot_mem_lowerBounds {α : Type u_1} [Preorder α] [OrderBot α] (s : Set α) : ⊥ ∈ lowerBounds s

@[simp]

theorem isLeast_bot_iff {α : Type u_1} [Preorder α] {s : Set α} [OrderBot α] : IsLeast s ⊥ ↔ ⊥ ∈ s

@[simp]

theorem isGreatest_top_iff {α : Type u_1} [Preorder α] {s : Set α} [OrderTop α] : IsGreatest s ⊤ ↔ ⊤ ∈ s

theorem not_bddAbove_iff' {α : Type u_1} [Preorder α] {s : Set α} : ¬BddAbove s ↔ ∀ (x : α), ∃ y ∈ s, ¬y ≤ x

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_bddBelow_iff' {α : Type u_1} [Preorder α] {s : Set α} : ¬BddBelow s ↔ ∀ (x : α), ∃ y ∈ s, ¬x ≤ y

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_bddAbove_iff {α : Type u_5} [LinearOrder α] {s : Set α} : ¬BddAbove s ↔ ∀ (x : α), ∃ y ∈ s, x < y

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_bddBelow_iff {α : Type u_5} [LinearOrder α] {s : Set α} : ¬BddBelow s ↔ ∀ (x : α), ∃ y ∈ s, y < x

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'.

@[simp]

theorem bddAbove_preimage_ofDual {α : Type u_1} [Preorder α] {s : Set α} : BddAbove (⇑OrderDual.ofDual ⁻¹' s) ↔ BddBelow s

@[simp]

theorem bddBelow_preimage_ofDual {α : Type u_1} [Preorder α] {s : Set α} : BddBelow (⇑OrderDual.ofDual ⁻¹' s) ↔ BddAbove s

@[simp]

theorem bddAbove_preimage_toDual {α : Type u_1} [Preorder α] {s : Set αᵒᵈ} : BddAbove (⇑OrderDual.toDual ⁻¹' s) ↔ BddBelow s

@[simp]

theorem bddBelow_preimage_toDual {α : Type u_1} [Preorder α] {s : Set αᵒᵈ} : BddBelow (⇑OrderDual.toDual ⁻¹' s) ↔ BddAbove s

theorem BddAbove.dual {α : Type u_1} [Preorder α] {s : Set α} (h : BddAbove s) : BddBelow (⇑OrderDual.ofDual ⁻¹' s)

theorem BddBelow.dual {α : Type u_1} [Preorder α] {s : Set α} (h : BddBelow s) : BddAbove (⇑OrderDual.ofDual ⁻¹' s)

theorem IsLeast.dual {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : IsGreatest (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)

theorem IsGreatest.dual {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : IsLeast (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)

theorem IsLUB.dual {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) : IsGLB (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)

theorem IsGLB.dual {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsGLB s a) : IsLUB (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)

@[reducible, inline]

abbrev IsLeast.orderBot {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : OrderBot ↑s

If a is the least element of a set s, then subtype s is an order with bottom element.

Equations

• h.orderBot = { bot := ⟨a, ⋯⟩, bot_le := ⋯ }

@[reducible, inline]

abbrev IsGreatest.orderTop {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : OrderTop ↑s

If a is the greatest element of a set s, then subtype s is an order with top element.

Equations

• h.orderTop = { top := ⟨a, ⋯⟩, le_top := ⋯ }

theorem isLUB_congr {α : Type u_1} [Preorder α] {s t : Set α} {a : α} (h : upperBounds s = upperBounds t) : IsLUB s a ↔ IsLUB t a

theorem isGLB_congr {α : Type u_1} [Preorder α] {s t : Set α} {a : α} (h : lowerBounds s = lowerBounds t) : IsGLB s a ↔ IsGLB t a

@[simp]

theorem IsCofinalFor.of_subset {α : Type u_1} [Preorder α] {s t : Set α} (hst : s ⊆ t) : IsCofinalFor s t

@[simp]

theorem IsCoinitialFor.of_subset {α : Type u_1} [Preorder α] {s t : Set α} (hst : s ⊆ t) : IsCoinitialFor s t

theorem LE.le.isCofinalFor {α : Type u_1} [Preorder α] {s t : Set α} (hst : s ⊆ t) : IsCofinalFor s t

Alias of IsCofinalFor.of_subset.

theorem LE.le.isCoinitialFor {α : Type u_1} [Preorder α] {s t : Set α} (hst : s ⊆ t) : IsCoinitialFor s t

Alias of IsCoinitialFor.of_subset.

theorem IsCofinalFor.rfl {α : Type u_1} [Preorder α] {s : Set α} : IsCofinalFor s s

theorem IsCoinitialFor.rfl {α : Type u_1} [Preorder α] {s : Set α} : IsCoinitialFor s s

theorem IsCofinalFor.trans {α : Type u_1} [Preorder α] {s t u : Set α} (hst : IsCofinalFor s t) (htu : IsCofinalFor t u) : IsCofinalFor s u

theorem IsCoinitialFor.trans {α : Type u_1} [Preorder α] {s t u : Set α} (hst : IsCoinitialFor s t) (htu : IsCoinitialFor t u) : IsCoinitialFor s u

theorem IsCofinalFor.mono_left {α : Type u_1} [Preorder α] {s t u : Set α} (hst : s ⊆ t) (htu : IsCofinalFor t u) : IsCofinalFor s u

theorem IsCoinitialFor.mono_left {α : Type u_1} [Preorder α] {s t u : Set α} (hst : s ⊆ t) (htu : IsCoinitialFor t u) : IsCoinitialFor s u

theorem IsCofinalFor.mono_right {α : Type u_1} [Preorder α] {s t u : Set α} (htu : t ⊆ u) (hst : IsCofinalFor s t) : IsCofinalFor s u

theorem IsCoinitialFor.mono_right {α : Type u_1} [Preorder α] {s t u : Set α} (htu : t ⊆ u) (hst : IsCoinitialFor s t) : IsCoinitialFor s u

theorem DirectedOn.isCofinalFor_fst_image_prod_snd_image {α : Type u_1} [Preorder α] {β : Type u_5} [Preorder β] {s : Set (α × β)} (hs : DirectedOn (fun (x1 x2 : α × β) => x1 ≤ x2) s) : IsCofinalFor ((Prod.fst '' s) ×ˢ (Prod.snd '' s)) s

theorem IsCofinalFor.nonempty {α : Type u_1} [Preorder α] {s t : Set α} (h : IsCofinalFor s t) (hs : s.Nonempty) : t.Nonempty

theorem IsCoinitialFor.nonempty {α : Type u_1} [Preorder α] {s t : Set α} (h : IsCoinitialFor s t) (hs : s.Nonempty) : t.Nonempty

theorem IsCofinalFor.union_left {α : Type u_1} [Preorder α] {s t : Set α} (hc : IsCofinalFor s t) : IsCofinalFor (s ∪ t) t

theorem IsCofinalFor.union_right {α : Type u_1} [Preorder α] {s t : Set α} (hc : IsCofinalFor s t) : IsCofinalFor (t ∪ s) t

theorem DirectedOn.of_isCofinalFor {α : Type u_1} [Preorder α] {s t : Set α} (hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) t) (hst : s ⊆ t) (hc : IsCofinalFor t s) : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s

theorem isCofinalFor_or_isCofinalFor_of_directedOn_union {α : Type u_1} [Preorder α] {s t : Set α} (h : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) (s ∪ t)) : IsCofinalFor t s ∨ IsCofinalFor s t

theorem directedOn_union_iff {α : Type u_1} [Preorder α] {s t : Set α} : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) (s ∪ t) ↔ DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s ∧ IsCofinalFor t s ∨ DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) t ∧ IsCofinalFor s t

theorem directedOn_or_directedOn_of_union {α : Type u_1} [Preorder α] {s t : Set α} (h : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) (s ∪ t)) : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s ∨ DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) t

theorem directedOn_or_directedOn_of_union' {α : Type u_1} [Preorder α] {s t : Set α} (hn : (s ∪ t).Nonempty) (h : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) (s ∪ t)) : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) t ∧ t.Nonempty

Monotonicity

theorem upperBounds_mono_set {α : Type u_1} [Preorder α] ⦃s t : Set α⦄ (hst : s ⊆ t) : upperBounds t ⊆ upperBounds s

theorem lowerBounds_mono_set {α : Type u_1} [Preorder α] ⦃s t : Set α⦄ (hst : s ⊆ t) : lowerBounds t ⊆ lowerBounds s

theorem upperBounds_mono_of_isCofinalFor {α : Type u_1} [Preorder α] {s t : Set α} (hst : IsCofinalFor s t) : upperBounds t ⊆ upperBounds s

theorem lowerBounds_mono_of_isCoinitialFor {α : Type u_1} [Preorder α] {s t : Set α} (hst : IsCoinitialFor s t) : lowerBounds t ⊆ lowerBounds s

theorem upperBounds_mono_mem {α : Type u_1} [Preorder α] {s : Set α} ⦃a b : α⦄ (hab : a ≤ b) : a ∈ upperBounds s → b ∈ upperBounds s

theorem lowerBounds_mono_mem {α : Type u_1} [Preorder α] {s : Set α} ⦃a b : α⦄ (hab : b ≤ a) : a ∈ lowerBounds s → b ∈ lowerBounds s

theorem upperBounds_mono {α : Type u_1} [Preorder α] ⦃s t : Set α⦄ (hst : s ⊆ t) ⦃a b : α⦄ (hab : a ≤ b) : a ∈ upperBounds t → b ∈ upperBounds s

theorem lowerBounds_mono {α : Type u_1} [Preorder α] ⦃s t : Set α⦄ (hst : s ⊆ t) ⦃a b : α⦄ (hab : b ≤ a) : a ∈ lowerBounds t → b ∈ lowerBounds s

theorem BddAbove.mono {α : Type u_1} [Preorder α] ⦃s t : Set α⦄ (h : s ⊆ t) : BddAbove t → BddAbove s

If s ⊆ t and t is bounded above, then so is s.

theorem BddBelow.mono {α : Type u_1} [Preorder α] ⦃s t : Set α⦄ (h : s ⊆ t) : BddBelow t → BddBelow s

If s ⊆ t and t is bounded below, then so is s.

theorem BddAbove.range_comp_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] (f : γ → β) {g : β → α} (hg : BddAbove (Set.range g)) : BddAbove (Set.range (g ∘ f))

If the range of a function g is bounded above, then g ∘ f is bounded above for all functions f.

theorem BddBelow.range_comp_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] (f : γ → β) {g : β → α} (hg : BddBelow (Set.range g)) : BddBelow (Set.range (g ∘ f))

If the range of a function g is bounded below, then g ∘ f is bounded below for all functions f.

theorem IsLUB.of_subset_of_superset {α : Type u_1} [Preorder α] {a : α} {s t p : Set α} (hs : IsLUB s a) (hp : IsLUB p a) (hst : s ⊆ t) (htp : t ⊆ p) : IsLUB t a

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 IsGLB.of_subset_of_superset {α : Type u_1} [Preorder α] {a : α} {s t p : Set α} (hs : IsGLB s a) (hp : IsGLB p a) (hst : s ⊆ t) (htp : t ⊆ p) : IsGLB t a

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 IsLUB.of_isCofinalFor {α : Type u_1} [Preorder α] {a : α} {s t : Set α} (hs : IsLUB s a) (hts : t ⊆ s) (hst : IsCofinalFor s t) : IsLUB t a

The least upper bound of a set is also the least upper bound of any cofinal subset.

theorem IsGLB.of_isCoinitialFor {α : Type u_1} [Preorder α] {a : α} {s t : Set α} (hs : IsGLB s a) (hts : t ⊆ s) (hst : IsCoinitialFor s t) : IsGLB t a

The greatest lower bound of a set is also the greatest lower bound of any coinitial subset.

theorem IsLeast.mono {α : Type u_1} [Preorder α] {s t : Set α} {a b : α} (ha : IsLeast s a) (hb : IsLeast t b) (hst : s ⊆ t) : b ≤ a

theorem IsGreatest.mono {α : Type u_1} [Preorder α] {s t : Set α} {a b : α} (ha : IsGreatest s a) (hb : IsGreatest t b) (hst : s ⊆ t) : a ≤ b

theorem IsLUB.mono {α : Type u_1} [Preorder α] {s t : Set α} {a b : α} (ha : IsLUB s a) (hb : IsLUB t b) (hst : s ⊆ t) : a ≤ b

theorem IsGLB.mono {α : Type u_1} [Preorder α] {s t : Set α} {a b : α} (ha : IsGLB s a) (hb : IsGLB t b) (hst : s ⊆ t) : b ≤ a

theorem subset_lowerBounds_upperBounds {α : Type u_1} [Preorder α] (s : Set α) : s ⊆ lowerBounds (upperBounds s)

theorem subset_upperBounds_lowerBounds {α : Type u_1} [Preorder α] (s : Set α) : s ⊆ upperBounds (lowerBounds s)

theorem Set.Nonempty.bddAbove_lowerBounds {α : Type u_1} [Preorder α] {s : Set α} (hs : s.Nonempty) : BddAbove (lowerBounds s)

theorem Set.Nonempty.bddBelow_upperBounds {α : Type u_1} [Preorder α] {s : Set α} (hs : s.Nonempty) : BddBelow (upperBounds s)

Conversions

theorem IsLeast.isGLB {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : IsGLB s a

theorem IsGreatest.isLUB {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : IsLUB s a

theorem IsGLB.isLeast {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsGLB s a) (hmem : a ∈ s) : IsLeast s a

theorem IsLUB.isGreatest {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) (hmem : a ∈ s) : IsGreatest s a

theorem isLeast_iff_isGLB_and_mem {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsLeast s a ↔ IsGLB s a ∧ a ∈ s

theorem isGreatest_iff_isLUB_and_mem {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsGreatest s a ↔ IsLUB s a ∧ a ∈ s

theorem IsLUB.upperBounds_eq {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) : upperBounds s = Set.Ici a

theorem IsGLB.lowerBounds_eq {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsGLB s a) : lowerBounds s = Set.Iic a

theorem IsLeast.lowerBounds_eq {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : lowerBounds s = Set.Iic a

theorem IsGreatest.upperBounds_eq {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : upperBounds s = Set.Ici a

theorem IsGreatest.lt_iff {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : IsGreatest s a) : a < b ↔ ∀ x ∈ s, x < b

theorem IsLeast.lt_iff {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : IsLeast s a) : b < a ↔ ∀ x ∈ s, b < x

theorem IsGreatest.le_iff {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : IsGreatest s a) : b ≤ a ↔ ∃ x ∈ s, b ≤ x

theorem IsLeast.le_iff {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : IsLeast s a) : a ≤ b ↔ ∃ x ∈ s, x ≤ b

theorem isLUB_le_iff {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : IsLUB s a) : a ≤ b ↔ b ∈ upperBounds s

theorem le_isGLB_iff {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : IsGLB s a) : b ≤ a ↔ b ∈ lowerBounds s

theorem isLUB_iff_le_iff {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsLUB s a ↔ ∀ (b : α), a ≤ b ↔ b ∈ upperBounds s

theorem isGLB_iff_le_iff {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsGLB s a ↔ ∀ (b : α), b ≤ a ↔ b ∈ lowerBounds s

theorem IsLUB.bddAbove {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) : BddAbove s

If s has a least upper bound, then it is bounded above.

theorem IsGLB.bddBelow {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsGLB s a) : BddBelow s

If s has a greatest lower bound, then it is bounded below.

theorem IsGreatest.bddAbove {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : BddAbove s

If s has a greatest element, then it is bounded above.

theorem IsLeast.bddBelow {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : BddBelow s

If s has a least element, then it is bounded below.

theorem IsLeast.nonempty {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : s.Nonempty

theorem IsGreatest.nonempty {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : s.Nonempty

Union and intersection

@[simp]

theorem upperBounds_union {α : Type u_1} [Preorder α] {s t : Set α} : upperBounds (s ∪ t) = upperBounds s ∩ upperBounds t

@[simp]

theorem lowerBounds_union {α : Type u_1} [Preorder α] {s t : Set α} : lowerBounds (s ∪ t) = lowerBounds s ∩ lowerBounds t

theorem union_upperBounds_subset_upperBounds_inter {α : Type u_1} [Preorder α] {s t : Set α} : upperBounds s ∪ upperBounds t ⊆ upperBounds (s ∩ t)

theorem union_lowerBounds_subset_lowerBounds_inter {α : Type u_1} [Preorder α] {s t : Set α} : lowerBounds s ∪ lowerBounds t ⊆ lowerBounds (s ∩ t)

theorem isLeast_union_iff {α : Type u_1} [Preorder α] {a : α} {s t : Set α} : IsLeast (s ∪ t) a ↔ IsLeast s a ∧ a ∈ lowerBounds t ∨ a ∈ lowerBounds s ∧ IsLeast t a

theorem isGreatest_union_iff {α : Type u_1} [Preorder α] {a : α} {s t : Set α} : IsGreatest (s ∪ t) a ↔ IsGreatest s a ∧ a ∈ upperBounds t ∨ a ∈ upperBounds s ∧ IsGreatest t a

theorem BddAbove.inter_of_left {α : Type u_1} [Preorder α] {s t : Set α} (h : BddAbove s) : BddAbove (s ∩ t)

If s is bounded, then so is s ∩ t

theorem BddBelow.inter_of_left {α : Type u_1} [Preorder α] {s t : Set α} (h : BddBelow s) : BddBelow (s ∩ t)

If s is bounded, then so is s ∩ t

theorem BddAbove.inter_of_right {α : Type u_1} [Preorder α] {s t : Set α} (h : BddAbove t) : BddAbove (s ∩ t)

If t is bounded, then so is s ∩ t

theorem BddBelow.inter_of_right {α : Type u_1} [Preorder α] {s t : Set α} (h : BddBelow t) : BddBelow (s ∩ t)

If t is bounded, then so is s ∩ t

theorem BddAbove.union {α : Type u_1} [Preorder α] [IsDirectedOrder α] {s t : Set α} : BddAbove s → BddAbove t → BddAbove (s ∪ t)

In a directed order, the union of bounded above sets is bounded above.

theorem BddBelow.union {α : Type u_1} [Preorder α] [IsCodirectedOrder α] {s t : Set α} : BddBelow s → BddBelow t → BddBelow (s ∪ t)

In a codirected order, the union of bounded below sets is bounded below.

theorem bddAbove_union {α : Type u_1} [Preorder α] [IsDirectedOrder α] {s t : Set α} : BddAbove (s ∪ t) ↔ BddAbove s ∧ BddAbove t

In a directed order, the union of two sets is bounded above if and only if both sets are.

theorem bddBelow_union {α : Type u_1} [Preorder α] [IsCodirectedOrder α] {s t : Set α} : BddBelow (s ∪ t) ↔ BddBelow s ∧ BddBelow t

In a codirected order, the union of two sets is bounded below if and only if both sets are.

theorem bbdAbove_range_sup {ι : Sort u_5} {α : Type u_6} [SemilatticeSup α] {f g : ι → α} (hf : BddAbove (Set.range f)) (hg : BddAbove (Set.range g)) : BddAbove (Set.range fun (x : ι) => f x ⊔ g x)

theorem bbdBelow_range_inf {ι : Sort u_5} {α : Type u_6} [SemilatticeInf α] {f g : ι → α} (hf : BddBelow (Set.range f)) (hg : BddBelow (Set.range g)) : BddBelow (Set.range fun (x : ι) => f x ⊓ g x)

theorem bbdAbove_range_left_of_sup {ι : Sort u_5} {α : Type u_6} [SemilatticeSup α] {f g : ι → α} (h : BddAbove (Set.range fun (x : ι) => f x ⊔ g x)) : BddAbove (Set.range f)

theorem bbdBelow_range_left_of_inf {ι : Sort u_5} {α : Type u_6} [SemilatticeInf α] {f g : ι → α} (h : BddBelow (Set.range fun (x : ι) => f x ⊓ g x)) : BddBelow (Set.range f)

theorem bbdAbove_range_right_of_sup {ι : Sort u_5} {α : Type u_6} [SemilatticeSup α] {f g : ι → α} (h : BddAbove (Set.range fun (x : ι) => f x ⊔ g x)) : BddAbove (Set.range g)

theorem bbdBelow_range_right_of_inf {ι : Sort u_5} {α : Type u_6} [SemilatticeInf α] {f g : ι → α} (h : BddBelow (Set.range fun (x : ι) => f x ⊓ g x)) : BddBelow (Set.range g)

theorem bbdAbove_range_sup_iff {ι : Sort u_5} {α : Type u_6} [SemilatticeSup α] {f g : ι → α} : BddAbove (Set.range fun (x : ι) => f x ⊔ g x) ↔ BddAbove (Set.range f) ∧ BddAbove (Set.range g)

theorem bbdBelow_range_inf_iff {ι : Sort u_5} {α : Type u_6} [SemilatticeInf α] {f g : ι → α} : BddBelow (Set.range fun (x : ι) => f x ⊓ g x) ↔ BddBelow (Set.range f) ∧ BddBelow (Set.range g)

theorem IsLUB.union {γ : Type u_3} [SemilatticeSup γ] {a b : γ} {s t : Set γ} (hs : IsLUB s a) (ht : IsLUB t b) : IsLUB (s ∪ t) (a ⊔ b)

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 IsGLB.union {γ : Type u_3} [SemilatticeInf γ] {a b : γ} {s t : Set γ} (hs : IsGLB s a) (ht : IsGLB t b) : IsGLB (s ∪ t) (a ⊓ b)

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 IsLeast.union {γ : Type u_3} [LinearOrder γ] {a b : γ} {s t : Set γ} (ha : IsLeast s a) (hb : IsLeast t b) : IsLeast (s ∪ t) (min a b)

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 IsGreatest.union {γ : Type u_3} [LinearOrder γ] {a b : γ} {s t : Set γ} (ha : IsGreatest s a) (hb : IsGreatest t b) : IsGreatest (s ∪ t) (max a b)

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 IsLUB.inter_Ici_of_mem {γ : Type u_3} [LinearOrder γ] {s : Set γ} {a b : γ} (ha : IsLUB s a) (hb : b ∈ s) : IsLUB (s ∩ Set.Ici b) a

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

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

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

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

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

Specific sets

Unbounded intervals

theorem isLeast_Ici {α : Type u_1} [Preorder α] {a : α} : IsLeast (Set.Ici a) a

theorem isGreatest_Iic {α : Type u_1} [Preorder α] {a : α} : IsGreatest (Set.Iic a) a

theorem isLUB_Iic {α : Type u_1} [Preorder α] {a : α} : IsLUB (Set.Iic a) a

theorem isGLB_Ici {α : Type u_1} [Preorder α] {a : α} : IsGLB (Set.Ici a) a

theorem upperBounds_Iic {α : Type u_1} [Preorder α] {a : α} : upperBounds (Set.Iic a) = Set.Ici a

theorem lowerBounds_Ici {α : Type u_1} [Preorder α] {a : α} : lowerBounds (Set.Ici a) = Set.Iic a

theorem bddAbove_Iic {α : Type u_1} [Preorder α] {a : α} : BddAbove (Set.Iic a)

theorem bddBelow_Ici {α : Type u_1} [Preorder α] {a : α} : BddBelow (Set.Ici a)

theorem bddAbove_Iio {α : Type u_1} [Preorder α] {a : α} : BddAbove (Set.Iio a)

theorem bddBelow_Ioi {α : Type u_1} [Preorder α] {a : α} : BddBelow (Set.Ioi a)

theorem le_of_isLUB_Iio {α : Type u_1} [Preorder α] {b : α} (a : α) (hb : IsLUB (Set.Iio a) b) : b ≤ a

theorem le_of_isGLB_Ioi {α : Type u_1} [Preorder α] {b : α} (a : α) (hb : IsGLB (Set.Ioi a) b) : a ≤ b

theorem lub_Iio_eq_self_or_Iio_eq_Iic {γ : Type u_3} [PartialOrder γ] {j : γ} (i : γ) (hj : IsLUB (Set.Iio i) j) : j = i ∨ Set.Iio i = Set.Iic j

theorem glb_Ioi_eq_self_or_Ioi_eq_Ici {γ : Type u_3} [PartialOrder γ] {j : γ} (i : γ) (hj : IsGLB (Set.Ioi i) j) : j = i ∨ Set.Ioi i = Set.Ici j

theorem exists_lub_Iio {γ : Type u_3} [LinearOrder γ] (i : γ) : ∃ (j : γ), IsLUB (Set.Iio i) j

theorem exists_glb_Ioi {γ : Type u_3} [LinearOrder γ] (i : γ) : ∃ (j : γ), IsGLB (Set.Ioi i) j

theorem isLUB_Iio {γ : Type u_3} [LinearOrder γ] [DenselyOrdered γ] {a : γ} : IsLUB (Set.Iio a) a

theorem isGLB_Ioi {γ : Type u_3} [LinearOrder γ] [DenselyOrdered γ] {a : γ} : IsGLB (Set.Ioi a) a

theorem upperBounds_Iio {γ : Type u_3} [LinearOrder γ] [DenselyOrdered γ] {a : γ} : upperBounds (Set.Iio a) = Set.Ici a

theorem lowerBounds_Ioi {γ : Type u_3} [LinearOrder γ] [DenselyOrdered γ] {a : γ} : lowerBounds (Set.Ioi a) = Set.Iic a

Singleton

@[simp]

theorem isGreatest_singleton {α : Type u_1} [Preorder α] {a : α} : IsGreatest {a} a

@[simp]

theorem isLeast_singleton {α : Type u_1} [Preorder α] {a : α} : IsLeast {a} a

@[simp]

theorem isLUB_singleton {α : Type u_1} [Preorder α] {a : α} : IsLUB {a} a

@[simp]

theorem isGLB_singleton {α : Type u_1} [Preorder α] {a : α} : IsGLB {a} a

@[simp]

theorem bddAbove_singleton {α : Type u_1} [Preorder α] {a : α} : BddAbove {a}

@[simp]

theorem bddBelow_singleton {α : Type u_1} [Preorder α] {a : α} : BddBelow {a}

@[simp]

theorem upperBounds_singleton {α : Type u_1} [Preorder α] {a : α} : upperBounds {a} = Set.Ici a

@[simp]

theorem lowerBounds_singleton {α : Type u_1} [Preorder α] {a : α} : lowerBounds {a} = Set.Iic a

Bounded intervals

@[simp]

theorem bddAbove_Icc {α : Type u_1} [Preorder α] {a b : α} : BddAbove (Set.Icc a b)

@[simp]

theorem bddBelow_Icc {α : Type u_1} [Preorder α] {a b : α} : BddBelow (Set.Icc b a)

@[simp]

theorem bddAbove_Ico {α : Type u_1} [Preorder α] {a b : α} : BddAbove (Set.Ico a b)

@[simp]

theorem bddBelow_Ioc {α : Type u_1} [Preorder α] {a b : α} : BddBelow (Set.Ioc b a)

@[simp]

theorem bddBelow_Ico {α : Type u_1} [Preorder α] {a b : α} : BddBelow (Set.Ico a b)

@[simp]

theorem bddAbove_Ioc {α : Type u_1} [Preorder α] {a b : α} : BddAbove (Set.Ioc b a)

@[simp]

theorem bddAbove_Ioo {α : Type u_1} [Preorder α] {a b : α} : BddAbove (Set.Ioo a b)

@[simp]

theorem bddBelow_Ioo {α : Type u_1} [Preorder α] {a b : α} : BddBelow (Set.Ioo b a)

theorem isGreatest_Icc {α : Type u_1} [Preorder α] {a b : α} (h : a ≤ b) : IsGreatest (Set.Icc a b) b

theorem isLeast_Icc {α : Type u_1} [Preorder α] {a b : α} (h : b ≤ a) : IsLeast (Set.Icc b a) b

theorem isLUB_Icc {α : Type u_1} [Preorder α] {a b : α} (h : a ≤ b) : IsLUB (Set.Icc a b) b

theorem isGLB_Icc {α : Type u_1} [Preorder α] {a b : α} (h : b ≤ a) : IsGLB (Set.Icc b a) b

theorem upperBounds_Icc {α : Type u_1} [Preorder α] {a b : α} (h : a ≤ b) : upperBounds (Set.Icc a b) = Set.Ici b

theorem lowerBounds_Icc {α : Type u_1} [Preorder α] {a b : α} (h : b ≤ a) : lowerBounds (Set.Icc b a) = Set.Iic b

theorem isGreatest_Ioc {α : Type u_1} [Preorder α] {a b : α} (h : a < b) : IsGreatest (Set.Ioc a b) b

theorem isLeast_Ico {α : Type u_1} [Preorder α] {a b : α} (h : b < a) : IsLeast (Set.Ico b a) b

theorem isLUB_Ioc {α : Type u_1} [Preorder α] {a b : α} (h : a < b) : IsLUB (Set.Ioc a b) b

theorem isGLB_Ico {α : Type u_1} [Preorder α] {a b : α} (h : b < a) : IsGLB (Set.Ico b a) b

theorem upperBounds_Ioc {α : Type u_1} [Preorder α] {a b : α} (h : a < b) : upperBounds (Set.Ioc a b) = Set.Ici b

theorem lowerBounds_Ico {α : Type u_1} [Preorder α] {a b : α} (h : b < a) : lowerBounds (Set.Ico b a) = Set.Iic b

theorem isGLB_Ioo {γ : Type u_3} [SemilatticeSup γ] [DenselyOrdered γ] {a b : γ} (h : a < b) : IsGLB (Set.Ioo a b) a

theorem isLUB_Ioo {γ : Type u_3} [SemilatticeInf γ] [DenselyOrdered γ] {a b : γ} (h : b < a) : IsLUB (Set.Ioo b a) a

theorem lowerBounds_Ioo {γ : Type u_3} [SemilatticeSup γ] [DenselyOrdered γ] {a b : γ} (hab : a < b) : lowerBounds (Set.Ioo a b) = Set.Iic a

theorem upperBounds_Ioo {γ : Type u_3} [SemilatticeInf γ] [DenselyOrdered γ] {a b : γ} (hab : b < a) : upperBounds (Set.Ioo b a) = Set.Ici a

theorem isGLB_Ioc {γ : Type u_3} [SemilatticeSup γ] [DenselyOrdered γ] {a b : γ} (hab : a < b) : IsGLB (Set.Ioc a b) a

theorem isLUB_Ico {γ : Type u_3} [SemilatticeInf γ] [DenselyOrdered γ] {a b : γ} (hab : b < a) : IsLUB (Set.Ico b a) a

theorem lowerBounds_Ioc {γ : Type u_3} [SemilatticeSup γ] [DenselyOrdered γ] {a b : γ} (hab : a < b) : lowerBounds (Set.Ioc a b) = Set.Iic a

theorem upperBounds_Ico {γ : Type u_3} [SemilatticeInf γ] [DenselyOrdered γ] {a b : γ} (hab : b < a) : upperBounds (Set.Ico b a) = Set.Ici a

theorem bddBelow_iff_subset_Ici {α : Type u_1} [Preorder α] {s : Set α} : BddBelow s ↔ ∃ (a : α), s ⊆ Set.Ici a

theorem bddAbove_iff_subset_Iic {α : Type u_1} [Preorder α] {s : Set α} : BddAbove s ↔ ∃ (a : α), s ⊆ Set.Iic a

theorem bddBelow_bddAbove_iff_subset_Icc {α : Type u_1} [Preorder α] {s : Set α} : BddBelow s ∧ BddAbove s ↔ ∃ (a : α) (b : α), s ⊆ Set.Icc a b

Univ

@[simp]

theorem mem_upperBounds_univ {α : Type u_1} [Preorder α] {a : α} : a ∈ upperBounds Set.univ ↔ IsTop a

@[simp]

theorem mem_lowerBounds_univ {α : Type u_1} [Preorder α] {a : α} : a ∈ lowerBounds Set.univ ↔ IsBot a

@[simp]

theorem isGreatest_univ_iff {α : Type u_1} [Preorder α] {a : α} : IsGreatest Set.univ a ↔ IsTop a

@[simp]

theorem isLeast_univ_iff {α : Type u_1} [Preorder α] {a : α} : IsLeast Set.univ a ↔ IsBot a

@[simp]

theorem isLUB_univ_iff {α : Type u_1} [Preorder α] {a : α} : IsLUB Set.univ a ↔ IsTop a

@[simp]

theorem isGLB_univ_iff {α : Type u_1} [Preorder α] {a : α} : IsGLB Set.univ a ↔ IsBot a

theorem isGreatest_univ {α : Type u_1} [Preorder α] [OrderTop α] : IsGreatest Set.univ ⊤

theorem isLeast_univ {α : Type u_1} [Preorder α] [OrderBot α] : IsLeast Set.univ ⊥

@[simp]

theorem OrderTop.upperBounds_univ {γ : Type u_3} [PartialOrder γ] [OrderTop γ] : upperBounds Set.univ = {⊤}

@[simp]

theorem OrderBot.lowerBounds_univ {γ : Type u_3} [PartialOrder γ] [OrderBot γ] : lowerBounds Set.univ = {⊥}

theorem isLUB_univ {α : Type u_1} [Preorder α] [OrderTop α] : IsLUB Set.univ ⊤

theorem isGLB_univ {α : Type u_1} [Preorder α] [OrderBot α] : IsGLB Set.univ ⊥

@[simp]

theorem NoTopOrder.upperBounds_univ {α : Type u_1} [Preorder α] [NoTopOrder α] : upperBounds Set.univ = ∅

@[simp]

theorem NoBotOrder.lowerBounds_univ {α : Type u_1} [Preorder α] [NoBotOrder α] : lowerBounds Set.univ = ∅

@[simp]

theorem not_bddAbove_univ {α : Type u_1} [Preorder α] [NoTopOrder α] : ¬BddAbove Set.univ

@[simp]

theorem not_bddBelow_univ {α : Type u_1} [Preorder α] [NoBotOrder α] : ¬BddBelow Set.univ

Empty set

@[simp]

theorem upperBounds_empty {α : Type u_1} [Preorder α] : upperBounds ∅ = Set.univ

@[simp]

theorem lowerBounds_empty {α : Type u_1} [Preorder α] : lowerBounds ∅ = Set.univ

@[simp]

theorem bddAbove_empty {α : Type u_1} [Preorder α] [Nonempty α] : BddAbove ∅

@[simp]

theorem bddBelow_empty {α : Type u_1} [Preorder α] [Nonempty α] : BddBelow ∅

@[simp]

theorem isGLB_empty_iff {α : Type u_1} [Preorder α] {a : α} : IsGLB ∅ a ↔ IsTop a

@[simp]

theorem isLUB_empty_iff {α : Type u_1} [Preorder α] {a : α} : IsLUB ∅ a ↔ IsBot a

theorem isGLB_empty {α : Type u_1} [Preorder α] [OrderTop α] : IsGLB ∅ ⊤

theorem isLUB_empty {α : Type u_1} [Preorder α] [OrderBot α] : IsLUB ∅ ⊥

theorem IsLUB.nonempty {α : Type u_1} [Preorder α] {s : Set α} {a : α} [NoBotOrder α] (hs : IsLUB s a) : s.Nonempty

theorem IsGLB.nonempty {α : Type u_1} [Preorder α] {s : Set α} {a : α} [NoTopOrder α] (hs : IsGLB s a) : s.Nonempty

theorem nonempty_of_not_bddAbove {α : Type u_1} [Preorder α] {s : Set α} [ha : Nonempty α] (h : ¬BddAbove s) : s.Nonempty

theorem nonempty_of_not_bddBelow {α : Type u_1} [Preorder α] {s : Set α} [ha : Nonempty α] (h : ¬BddBelow s) : s.Nonempty

insert

@[simp]

theorem bddAbove_insert {α : Type u_1} [Preorder α] [IsDirectedOrder α] {s : Set α} {a : α} : BddAbove (insert a s) ↔ BddAbove s

Adding a point to a set preserves its boundedness above.

@[simp]

theorem bddBelow_insert {α : Type u_1} [Preorder α] [IsCodirectedOrder α] {s : Set α} {a : α} : BddBelow (insert a s) ↔ BddBelow s

Adding a point to a set preserves its boundedness below.

theorem BddAbove.insert {α : Type u_1} [Preorder α] [IsDirectedOrder α] {s : Set α} (a : α) : BddAbove s → BddAbove (insert a s)

theorem BddBelow.insert {α : Type u_1} [Preorder α] [IsCodirectedOrder α] {s : Set α} (a : α) : BddBelow s → BddBelow (insert a s)

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

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

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

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

@[simp]

theorem upperBounds_insert {α : Type u_1} [Preorder α] (a : α) (s : Set α) : upperBounds (insert a s) = Set.Ici a ∩ upperBounds s

@[simp]

theorem lowerBounds_insert {α : Type u_1} [Preorder α] (a : α) (s : Set α) : lowerBounds (insert a s) = Set.Iic a ∩ lowerBounds s

@[simp]

theorem OrderTop.bddAbove {α : Type u_1} [Preorder α] [OrderTop α] (s : Set α) : BddAbove s

When there is a global maximum, every set is bounded above.

@[simp]

theorem OrderBot.bddBelow {α : Type u_1} [Preorder α] [OrderBot α] (s : Set α) : BddBelow s

When there is a global minimum, every set is bounded below.

def tacticBddDefault : Lean.ParserDescr

Sets are automatically bounded or cobounded in complete lattices. To use the same statements in complete and conditionally complete lattices but let automation fill automatically the boundedness proofs in complete lattices, we use the tactic bddDefault in the statements, in the form (hA : BddAbove A := by bddDefault).

Equations

• tacticBddDefault = Lean.ParserDescr.node `tacticBddDefault 1024 (Lean.ParserDescr.nonReservedSymbol "bddDefault" false)

Pair

theorem isLUB_pair {γ : Type u_3} [SemilatticeSup γ] {a b : γ} : IsLUB {a, b} (a ⊔ b)

theorem isGLB_pair {γ : Type u_3} [SemilatticeInf γ] {a b : γ} : IsGLB {a, b} (a ⊓ b)

theorem isGreatest_pair {γ : Type u_3} [LinearOrder γ] {a b : γ} : IsGreatest {a, b} (max a b)

theorem isLeast_pair {γ : Type u_3} [LinearOrder γ] {a b : γ} : IsLeast {a, b} (min a b)

Lower/upper bounds

@[simp]

theorem isLUB_lowerBounds {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsLUB (lowerBounds s) a ↔ IsGLB s a

@[simp]

theorem isGLB_upperBounds {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsGLB (upperBounds s) a ↔ IsLUB s a

theorem IsLUB.isLUB_sSup {α : Type u_1} [Preorder α] [OrderSupSet α] {s : Set α} {a : α} : IsLUB s a → IsLUB s (sSup s)

theorem IsGLB.isGLB_sInf {α : Type u_1} [Preorder α] [OrderInfSet α] {s : Set α} {a : α} : IsGLB s a → IsGLB s (sInf s)

theorem exists_isLUB_iff_isLUB_sSup {α : Type u_1} [Preorder α] [OrderSupSet α] {s : Set α} : (∃ (a : α), IsLUB s a) ↔ IsLUB s (sSup s)

theorem exists_isGLB_iff_isGLB_sInf {α : Type u_1} [Preorder α] [OrderInfSet α] {s : Set α} : (∃ (a : α), IsGLB s a) ↔ IsGLB s (sInf s)

@[reducible, inline]

abbrev OrderInfSet.ofOrderSupSet {α : Type u_1} [Preorder α] [OrderSupSet α] : OrderInfSet α

Constructs an OrderInfSet from an OrderSupSet by defining the infimum of a set as the supremum of its lower bounds.

Equations

• OrderInfSet.ofOrderSupSet = { sInf := fun (s : Set α) => sSup (lowerBounds s), isGLB_sInf_of_isGLB := ⋯ }

@[reducible, inline]

abbrev OrderSupSet.ofOrderInfSet {α : Type u_1} [Preorder α] [OrderInfSet α] : OrderSupSet α

Constructs an OrderSupSet from an OrderInfSet by defining the supremum of a set as the infimum of its upper bounds.

Equations

• OrderSupSet.ofOrderInfSet = { sSup := fun (s : Set α) => sInf (upperBounds s), isLUB_sSup_of_isLUB := ⋯ }

@[instance_reducible]

noncomputable def OrderSupSet.choose {α : Type u_1} [Preorder α] (d : α) : OrderSupSet α

Noncomputably constructs a "supremum" for an arbitrary set using the axiom of choice such that it is the actual supremum of the set if one exists, and the default value d otherwise.

Equations

• OrderSupSet.choose d = { sSup := fun (s : Set α) => if h : ∃ (x : α), IsLUB s x then h.choose else d, isLUB_sSup_of_isLUB := ⋯ }

@[instance_reducible]

noncomputable def OrderInfSet.choose {α : Type u_1} [Preorder α] (d : α) : OrderInfSet α

Noncomputably constructs an "infimum" for an arbitrary set using the axiom of choice such that it is the actual infimum of the set if one exists, and the default value d otherwise.

Equations

• OrderInfSet.choose d = { sInf := fun (s : Set α) => if h : ∃ (x : α), IsGLB s x then h.choose else d, isGLB_sInf_of_isGLB := ⋯ }

theorem OrderInfSet.choose_sInf {α : Type u_1} [Preorder α] (d : α) (s : Set α) : sInf s = if h : ∃ (x : α), IsGLB s x then h.choose else d

theorem OrderSupSet.choose_sSup {α : Type u_1} [Preorder α] (d : α) (s : Set α) : sSup s = if h : ∃ (x : α), IsLUB s x then h.choose else d

@[instance_reducible]

noncomputable def OrderSupSet.chooseBot {α : Type u_1} [Preorder α] (d : α) : OrderSupSet α

Noncomputably constructs a "supremum" for an arbitrary set using the axiom of choice such that it is the actual supremum of the set if one exists, the bottom element if the supremum doesn't exist but a bottom element does, and the default value d if neither exists.

The junk value satisfies sSup s = sSup ∅ for any set s without a supremum, which is the same as the convention of ConditionallyCompleteLinearOrder.

Equations

• OrderSupSet.chooseBot d = OrderSupSet.choose (sSup ∅)

@[instance_reducible]

noncomputable def OrderInfSet.chooseTop {α : Type u_1} [Preorder α] (d : α) : OrderInfSet α

Noncomputably constructs an "infimum" for an arbitrary set using the axiom of choice such that it is the actual infimum of the set if one exists, the top element if the infimum doesn't exist but a top element does, and the default value d if neither exists.

The junk value satisfies sInf s = sInf ∅ for any set s without an infimum, which is the same as the convention of ConditionallyCompleteLinearOrder.

Equations

• OrderInfSet.chooseTop d = OrderInfSet.choose (sInf ∅)

theorem OrderSupSet.chooseBot_sSup_of_not_exists {α : Type u_1} [Preorder α] {d : α} {s : Set α} (h : ¬∃ (x : α), IsLUB s x) : sSup s = sSup ∅

theorem OrderInfSet.chooseTop_sInf_of_not_exists {α : Type u_1} [Preorder α] {d : α} {s : Set α} (h : ¬∃ (x : α), IsGLB s x) : sInf s = sInf ∅

theorem OrderSupSet.chooseBot_sSup_empty_of_noBotOrder {α : Type u_1} [Preorder α] [NoBotOrder α] {d : α} : sSup ∅ = d

theorem OrderInfSet.chooseTop_sInf_empty_of_noTopOrder {α : Type u_1} [Preorder α] [NoTopOrder α] {d : α} : sInf ∅ = d

theorem DirectedOn.le_of_minimal {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : DirectedOn (fun (x y : α) => y ≤ x) s) (hMin : Minimal (fun (x : α) => x ∈ s) a) (hb : b ∈ s) : a ≤ b

theorem DirectedOn.le_of_maximal {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : DirectedOn (fun (x y : α) => x ≤ y) s) (hMax : Maximal (fun (x : α) => x ∈ s) a) (hb : b ∈ s) : b ≤ a

theorem DirectedOn.minimal_iff_isLeast {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : DirectedOn (fun (x y : α) => y ≤ x) s) : Minimal (fun (x : α) => x ∈ s) a ↔ IsLeast s a

theorem DirectedOn.maximal_iff_isGreatest {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : DirectedOn (fun (x y : α) => x ≤ y) s) : Maximal (fun (x : α) => x ∈ s) a ↔ IsGreatest s a

theorem minimal_iff_isLeast {α : Type u_1} [LinearOrder α] {s : Set α} {a : α} : Minimal (fun (x : α) => x ∈ s) a ↔ IsLeast s a

theorem maximal_iff_isGreatest {α : Type u_1} [LinearOrder α] {s : Set α} {a : α} : Maximal (fun (x : α) => x ∈ s) a ↔ IsGreatest s a

(In)equalities with the least upper bound and the greatest lower bound

theorem lowerBounds_le_upperBounds {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds s) : s.Nonempty → a ≤ b

theorem lowerBounds_le_upperBounds_of_nonempty_inter {α : Type u_1} [Preorder α] {s s' : Set α} {a b : α} (h : (s ∩ s').Nonempty) (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds s') : a ≤ b

theorem isGLB_le_isLUB {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (ha : IsGLB s a) (hb : IsLUB s b) (hs : s.Nonempty) : a ≤ b

theorem isGLB_le_isLUB_of_nonempty_inter {α : Type u_1} [Preorder α] {s s' : Set α} {a b : α} (h : (s ∩ s').Nonempty) (ha : IsGLB s a) (hb : IsLUB s' b) : a ≤ b

theorem isLUB_lt_iff {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (ha : IsLUB s a) : a < b ↔ ∃ c ∈ upperBounds s, c < b

theorem lt_isGLB_iff {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (ha : IsGLB s a) : b < a ↔ ∃ c ∈ lowerBounds s, b < c

theorem le_of_isLUB_le_isGLB {α : Type u_1} [Preorder α] {s : Set α} {a b x y : α} (ha : IsGLB s a) (hb : IsLUB s b) (hab : b ≤ a) (hx : x ∈ s) (hy : y ∈ s) : x ≤ y

@[simp]

theorem upperBounds_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) : upperBounds (s ×ˢ t) = upperBounds s ×ˢ upperBounds t

@[simp]

theorem lowerBounds_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) : lowerBounds (s ×ˢ t) = lowerBounds s ×ˢ lowerBounds t

theorem IsLUB.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} {a : α} {b : β} (hs : s.Nonempty) (ht : t.Nonempty) (ha : IsLUB s a) (hb : IsLUB t b) : IsLUB (s ×ˢ t) (a, b)

theorem IsGLB.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} {a : α} {b : β} (hs : s.Nonempty) (ht : t.Nonempty) (ha : IsGLB s a) (hb : IsGLB t b) : IsGLB (s ×ˢ t) (a, b)

theorem isLUB_congr_of_antisymmRel {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b) : IsLUB s a ↔ IsLUB s b

theorem isGLB_congr_of_antisymmRel {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b) : IsGLB s a ↔ IsGLB s b

theorem IsLeast.unique {α : Type u_1} [PartialOrder α] {s : Set α} {a b : α} (Ha : IsLeast s a) (Hb : IsLeast s b) : a = b

theorem IsGreatest.unique {α : Type u_1} [PartialOrder α] {s : Set α} {a b : α} (Ha : IsGreatest s a) (Hb : IsGreatest s b) : a = b

theorem IsLeast.isLeast_iff_eq {α : Type u_1} [PartialOrder α] {s : Set α} {a b : α} (Ha : IsLeast s a) : IsLeast s b ↔ a = b

theorem IsGreatest.isGreatest_iff_eq {α : Type u_1} [PartialOrder α] {s : Set α} {a b : α} (Ha : IsGreatest s a) : IsGreatest s b ↔ a = b

theorem IsLUB.unique {α : Type u_1} [PartialOrder α] {s : Set α} {a b : α} (Ha : IsLUB s a) (Hb : IsLUB s b) : a = b

theorem IsGLB.unique {α : Type u_1} [PartialOrder α] {s : Set α} {a b : α} (Ha : IsGLB s a) (Hb : IsGLB s b) : a = b

theorem IsLUB.sSup_eq {α : Type u_1} [PartialOrder α] [OrderSupSet α] {s : Set α} {a : α} (h : IsLUB s a) : sSup s = a

theorem IsGLB.sInf_eq {α : Type u_1} [PartialOrder α] [OrderInfSet α] {s : Set α} {a : α} (h : IsGLB s a) : sInf s = a

theorem IsLUB.iSup_eq {α : Type u_1} {ι : Sort u_4} [PartialOrder α] [OrderSupSet α] {f : ι → α} {a : α} (h : IsLUB (Set.range f) a) : iSup f = a

theorem IsGLB.iInf_eq {α : Type u_1} {ι : Sort u_4} [PartialOrder α] [OrderInfSet α] {f : ι → α} {a : α} (h : IsGLB (Set.range f) a) : iInf f = a

@[simp]

theorem sSup_singleton {α : Type u_1} [PartialOrder α] [OrderSupSet α] {a : α} : sSup {a} = a

@[simp]

theorem sInf_singleton {α : Type u_1} [PartialOrder α] [OrderInfSet α] {a : α} : sInf {a} = a

@[simp]

theorem sSup_empty {α : Type u_1} [PartialOrder α] [OrderSupSet α] [OrderBot α] : sSup ∅ = ⊥

@[simp]

theorem sInf_empty {α : Type u_1} [PartialOrder α] [OrderInfSet α] [OrderTop α] : sInf ∅ = ⊤

@[simp]

theorem sSup_univ {α : Type u_1} [PartialOrder α] [OrderSupSet α] [OrderTop α] : sSup Set.univ = ⊤

@[simp]

theorem sInf_univ {α : Type u_1} [PartialOrder α] [OrderInfSet α] [OrderBot α] : sInf Set.univ = ⊥

theorem sSup_pair {α : Type u_5} [SemilatticeSup α] [OrderSupSet α] {a b : α} : sSup {a, b} = a ⊔ b

theorem sInf_pair {α : Type u_5} [SemilatticeInf α] [OrderInfSet α] {a b : α} : sInf {a, b} = a ⊓ b

@[simp]

theorem iSup_of_empty' {α : Type u_5} {ι : Sort u_6} [SupSet α] [IsEmpty ι] (f : ι → α) : iSup f = sSup ∅

This simp lemma goes well with sSup_empty in a complete lattice.

@[simp]

theorem iInf_of_isEmpty {α : Type u_5} {ι : Sort u_6} [InfSet α] [IsEmpty ι] (f : ι → α) : iInf f = sInf ∅

This simp lemma goes well with sInf_empty in a complete lattice.

theorem iSup_of_empty {α : Type u_1} {ι : Sort u_4} [PartialOrder α] [OrderSupSet α] [OrderBot α] [IsEmpty ι] (f : ι → α) : iSup f = ⊥

theorem iInf_of_empty {α : Type u_1} {ι : Sort u_4} [PartialOrder α] [OrderInfSet α] [OrderTop α] [IsEmpty ι] (f : ι → α) : iInf f = ⊤

theorem iSup_const {α : Type u_1} {ι : Sort u_4} [PartialOrder α] {a : α} [OrderSupSet α] [Nonempty ι] : ⨆ (x : ι), a = a

theorem iInf_const {α : Type u_1} {ι : Sort u_4} [PartialOrder α] {a : α} [OrderInfSet α] [Nonempty ι] : ⨅ (x : ι), a = a

theorem iSup_const_le {α : Type u_1} {ι : Sort u_4} [PartialOrder α] {a : α} [OrderSupSet α] [OrderBot α] : ⨆ (x : ι), a ≤ a

theorem le_iInf_const {α : Type u_1} {ι : Sort u_4} [PartialOrder α] {a : α} [OrderInfSet α] [OrderTop α] : a ≤ ⨅ (x : ι), a

theorem iSup_unique {α : Type u_1} {ι : Sort u_4} [PartialOrder α] [OrderSupSet α] [Unique ι] (f : ι → α) : ⨆ (i : ι), f i = f default

theorem iInf_unique {α : Type u_1} {ι : Sort u_4} [PartialOrder α] [OrderInfSet α] [Unique ι] (f : ι → α) : ⨅ (i : ι), f i = f default

@[simp]

theorem iSup_bot {α : Type u_1} {ι : Sort u_4} [PartialOrder α] [OrderSupSet α] [OrderBot α] : ⨆ (x : ι), ⊥ = ⊥

@[simp]

theorem iInf_top {α : Type u_1} {ι : Sort u_4} [PartialOrder α] [OrderInfSet α] [OrderTop α] : ⨅ (x : ι), ⊤ = ⊤

theorem Set.subsingleton_of_isLUB_le_isGLB {α : Type u_1} [PartialOrder α] {s : Set α} {a b : α} (Ha : IsGLB s a) (Hb : IsLUB s b) (hab : b ≤ a) : s.Subsingleton

theorem isGLB_lt_isLUB_of_ne {α : Type u_1} [PartialOrder α] {s : Set α} {a b : α} (Ha : IsGLB s a) (Hb : IsLUB s b) {x y : α} (Hx : x ∈ s) (Hy : y ∈ s) (Hxy : x ≠ y) : a < b

theorem lt_isLUB_iff {α : Type u_1} [LinearOrder α] {s : Set α} {a b : α} (h : IsLUB s a) : b < a ↔ ∃ c ∈ s, b < c

theorem isGLB_lt_iff {α : Type u_1} [LinearOrder α] {s : Set α} {a b : α} (h : IsGLB s a) : a < b ↔ ∃ c ∈ s, c < b

theorem IsLUB.exists_between {α : Type u_1} [LinearOrder α] {s : Set α} {a b : α} (h : IsLUB s a) (hb : b < a) : ∃ c ∈ s, b < c ∧ c ≤ a

theorem IsLUB.exists_between' {α : Type u_1} [LinearOrder α] {s : Set α} {a b : α} (h : IsLUB s a) (h' : a ∉ s) (hb : b < a) : ∃ c ∈ s, b < c ∧ c < a

theorem IsGLB.exists_between {α : Type u_1} [LinearOrder α] {s : Set α} {a b : α} (h : IsGLB s a) (hb : a < b) : ∃ c ∈ s, a ≤ c ∧ c < b

theorem IsGLB.exists_between' {α : Type u_1} [LinearOrder α] {s : Set α} {a b : α} (h : IsGLB s a) (h' : a ∉ s) (hb : a < b) : ∃ c ∈ s, a < c ∧ c < b

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

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

theorem isGreatest_compl {α : Type u_1} [HeytingAlgebra α] (a : α) : IsGreatest {w : α | Disjoint w a} aᶜ

theorem isLeast_hnot {α : Type u_1} [CoheytingAlgebra α] (a : α) : IsLeast {w : α | Codisjoint a w} (￢a)

@[instance_reducible]

instance Nat.instDecidableIsLeast (p : ℕ → Prop) (n : ℕ) [DecidablePred p] : Decidable (IsLeast {n : ℕ | p n} n)

Equations

• Nat.instDecidableIsLeast p n = decidable_of_iff (p n ∧ ∀ k < n, ¬p k) ⋯

@[instance_reducible]

def SemilatticeSup.ofIsLUB {α : Type u_1} [PartialOrder α] (sup : α → α → α) (isLUB_pair : ∀ (a b : α), IsLUB {a, b} (sup a b)) : SemilatticeSup α

An alternative constructor for SemilatticeSup using IsLUB.

Equations

• SemilatticeSup.ofIsLUB sup isLUB_pair = { toPartialOrder := inst✝, sup := sup, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯ }

@[instance_reducible]

def SemilatticeInf.ofIsGLB {α : Type u_1} [PartialOrder α] (inf : α → α → α) (isGLB_pair : ∀ (a b : α), IsGLB {a, b} (inf a b)) : SemilatticeInf α

An alternative constructor for SemilatticeInf using IsGLB.

Equations

• SemilatticeInf.ofIsGLB sup isLUB_pair = { toPartialOrder := inst✝, inf := sup, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

@[instance_reducible]

def Lattice.ofIsLUBofIsGLB {α : Type u_1} [PartialOrder α] (sup inf : α → α → α) (isLUB_pair : ∀ (a b : α), IsLUB {a, b} (sup a b)) (isGLB_pair : ∀ (a b : α), IsGLB {a, b} (inf a b)) : Lattice α

An alternative constructor for Lattice using IsLUB and IsGLB.

Equations

• Lattice.ofIsLUBofIsGLB sup inf isLUB_pair isGLB_pair = { toSemilatticeSup := SemilatticeSup.ofIsLUB sup isLUB_pair, inf := SemilatticeInf.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }