Loogle!

Result

Found 230 declarations mentioning IsLUB. Of these, only the first 200 are shown.

• IsLUB 📋 Mathlib.Order.Bounds.Defs
  {α : Type u_1} [LE α] (s : Set α) : α → Prop
• isLUB_Iic 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a : α} : IsLUB (Set.Iic a) a
• isLUB_singleton 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a : α} : IsLUB {a} a
• isLUB_univ_iff 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a : α} : IsLUB Set.univ a ↔ IsTop a
• IsLUB.bddAbove 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) : BddAbove s
• IsGreatest.isLUB 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : IsLUB s a
• IsLUB.nonempty 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} [NoBotOrder α] (hs : IsLUB s a) : s.Nonempty
• isLUB_empty_iff 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a : α} : IsLUB ∅ a ↔ IsBot a
• le_of_isLUB_Iio 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {b : α} (a : α) (hb : IsLUB (Set.Iio a) b) : b ≤ a
• isLUB_Icc 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a b : α} (h : a ≤ b) : IsLUB (Set.Icc a b) b
• isLUB_Ioc 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a b : α} (h : a < b) : IsLUB (Set.Ioc a b) b
• isLUB_univ 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] [OrderTop α] : IsLUB Set.univ ⊤
• isGLB_upperBounds 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsGLB (upperBounds s) a ↔ IsLUB s a
• isLUB_empty 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] [OrderBot α] : IsLUB ∅ ⊥
• isLUB_lowerBounds 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsLUB (lowerBounds s) a ↔ IsGLB s a
• IsLUB.upperBounds_eq 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) : upperBounds s = Set.Ici a
• IsLUB.isGreatest 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) (hmem : a ∈ s) : IsGreatest s a
• IsLUB.unique 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [PartialOrder α] {s : Set α} {a b : α} (Ha : IsLUB s a) (Hb : IsLUB s b) : a = b
• isGreatest_iff_isLUB_and_mem 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsGreatest s a ↔ IsLUB s a ∧ a ∈ s
• isGLB_le_isLUB 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (ha : IsGLB s a) (hb : IsLUB s b) (hs : s.Nonempty) : a ≤ b
• SemilatticeSup.ofIsLUB 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [PartialOrder α] (sup : α → α → α) (isLUB_pair : ∀ (a b : α), IsLUB {a, b} (sup a b)) : SemilatticeSup α
• isLUB_congr_of_antisymmRel 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : AntisymmRel (fun x1 x2 => x1 ≤ x2) a b) : IsLUB s a ↔ IsLUB s b
• isLUB_le_iff 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : IsLUB s a) : a ≤ b ↔ b ∈ upperBounds s
• isLUB_pair 📋 Mathlib.Order.Bounds.Basic
  {γ : Type u_3} [SemilatticeSup γ] {a b : γ} : IsLUB {a, b} (a ⊔ b)
• isLUB_iff_le_iff 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsLUB s a ↔ ∀ (b : α), a ≤ b ↔ b ∈ upperBounds s
• IsLUB.of_isCofinalFor 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a : α} {s t : Set α} (hs : IsLUB s a) (hts : t ⊆ s) (hst : IsCofinalFor s t) : IsLUB t a
• exists_lub_Iio 📋 Mathlib.Order.Bounds.Basic
  {γ : Type u_3} [LinearOrder γ] (i : γ) : ∃ j, IsLUB (Set.Iio i) j
• IsLUB.mono 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s t : Set α} {a b : α} (ha : IsLUB s a) (hb : IsLUB t b) (hst : s ⊆ t) : a ≤ b
• Set.subsingleton_of_isLUB_le_isGLB 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [PartialOrder α] {s : Set α} {a b : α} (Ha : IsGLB s a) (Hb : IsLUB s b) (hab : b ≤ a) : s.Subsingleton
• isLUB_congr 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s t : Set α} {a : α} (h : upperBounds s = upperBounds t) : IsLUB s a ↔ IsLUB t a
• isGLB_le_isLUB_of_nonempty_inter 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s s' : Set α} {a b : α} (h : (s ∩ s').Nonempty) (ha : IsGLB s a) (hb : IsLUB s' b) : a ≤ b
• lub_Iio_eq_self_or_Iio_eq_Iic 📋 Mathlib.Order.Bounds.Basic
  {γ : Type u_3} [PartialOrder γ] {j : γ} (i : γ) (hj : IsLUB (Set.Iio i) j) : j = i ∨ Set.Iio i = Set.Iic j
• IsLUB.insert 📋 Mathlib.Order.Bounds.Basic
  {γ : Type u_3} [SemilatticeSup γ] (a : γ) {b : γ} {s : Set γ} (hs : IsLUB s b) : IsLUB (insert a s) (a ⊔ b)
• isLUB_Ico 📋 Mathlib.Order.Bounds.Basic
  {γ : Type u_3} [SemilatticeInf γ] [DenselyOrdered γ] {a b : γ} (hab : b < a) : IsLUB (Set.Ico b a) a
• isLUB_Ioo 📋 Mathlib.Order.Bounds.Basic
  {γ : Type u_3} [SemilatticeInf γ] [DenselyOrdered γ] {a b : γ} (h : b < a) : IsLUB (Set.Ioo b a) a
• IsLUB.of_subset_of_superset 📋 Mathlib.Order.Bounds.Basic
  {α : 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
• isLUB_lt_iff 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (ha : IsLUB s a) : a < b ↔ ∃ c ∈ upperBounds s, c < b
• isLUB_Iio 📋 Mathlib.Order.Bounds.Basic
  {γ : Type u_3} [LinearOrder γ] [DenselyOrdered γ] {a : γ} : IsLUB (Set.Iio a) a
• le_of_isLUB_le_isGLB 📋 Mathlib.Order.Bounds.Basic
  {α : 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
• IsLUB.union 📋 Mathlib.Order.Bounds.Basic
  {γ : Type u_3} [SemilatticeSup γ] {a b : γ} {s t : Set γ} (hs : IsLUB s a) (ht : IsLUB t b) : IsLUB (s ∪ t) (a ⊔ b)
• isGLB_lt_isLUB_of_ne 📋 Mathlib.Order.Bounds.Basic
  {α : 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
• Lattice.ofIsLUBofIsGLB 📋 Mathlib.Order.Bounds.Basic
  {α : 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 α
• IsLUB.prod 📋 Mathlib.Order.Bounds.Basic
  {α : 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)
• IsLUB.inter_Ici_of_mem 📋 Mathlib.Order.Bounds.Basic
  {γ : Type u_3} [LinearOrder γ] {s : Set γ} {a b : γ} (ha : IsLUB s a) (hb : b ∈ s) : IsLUB (s ∩ Set.Ici b) a
• lt_isLUB_iff 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [LinearOrder α] {s : Set α} {a b : α} (h : IsLUB s a) : b < a ↔ ∃ c ∈ s, b < c
• IsGLB.dual 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsGLB s a) : IsLUB (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
• IsLUB.dual 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) : IsGLB (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
• IsLUB.exists_between 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [LinearOrder α] {s : Set α} {a b : α} (h : IsLUB s a) (hb : b < a) : ∃ c ∈ s, b < c ∧ c ≤ a
• IsLUB.exists_between' 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [LinearOrder α] {s : Set α} {a b : α} (h : IsLUB s a) (h' : a ∉ s) (hb : b < a) : ∃ c ∈ s, b < c ∧ c < a
• IsLUB.of_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : ∀ {x y : α}, f y ≤ f x ↔ y ≤ x) {s : Set α} {x : α} (hx : IsLUB (f '' s) (f x)) : IsLUB s x
• isLUB_pi 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {π : α → Type u_1} [(a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} {f : (a : α) → π a} : IsLUB s f ↔ ∀ (a : α), IsLUB (Function.eval a '' s) (f a)
• isLUB_prod 📋 Mathlib.Order.Bounds.Image
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set (α × β)} {p : α × β} : IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
• OrderIso.isLUB_image' 📋 Mathlib.Order.Bounds.OrderIso
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) {s : Set α} {x : α} : IsLUB (⇑f '' s) (f x) ↔ IsLUB s x
• OrderIso.isLUB_preimage 📋 Mathlib.Order.Bounds.OrderIso
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) {s : Set β} {x : α} : IsLUB (⇑f ⁻¹' s) x ↔ IsLUB s (f x)
• OrderIso.isLUB_image 📋 Mathlib.Order.Bounds.OrderIso
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) {s : Set α} {x : β} : IsLUB (⇑f '' s) x ↔ IsLUB s (f.symm x)
• OrderIso.isLUB_preimage' 📋 Mathlib.Order.Bounds.OrderIso
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) {s : Set β} {x : β} : IsLUB (⇑f ⁻¹' s) (f.symm x) ↔ IsLUB s x
• IsLUB.mul_left 📋 Mathlib.Algebra.Order.Field.Basic
  {α : Type u_1} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α] {s : Set α} (ha : 0 ≤ a) (hs : IsLUB s b) : IsLUB ((fun b => a * b) '' s) (a * b)
• IsLUB.mul_right 📋 Mathlib.Algebra.Order.Field.Basic
  {α : Type u_1} [Semifield α] [PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α] {s : Set α} (ha : 0 ≤ a) (hs : IsLUB s b) : IsLUB ((fun b => b * a) '' s) (b * a)
• completeLatticeOfSup 📋 Mathlib.Order.CompleteLattice.Defs
  (α : Type u_4) [H1 : PartialOrder α] [H2 : SupSet α] (isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)) : CompleteLattice α
• isLUB_sSup 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeSup α] (s : Set α) : IsLUB s (sSup s)
• CompleteSemilatticeSup.isLUB_sSup 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_4} [self : CompleteSemilatticeSup α] (s : Set α) : IsLUB s (sSup s)
• CompleteSemilatticeSup.mk 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_4} [toPartialOrder : PartialOrder α] [toSupSet : SupSet α] (isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)) : CompleteSemilatticeSup α
• CompleteLattice.isLUB_sSup 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_4} [self : CompleteLattice α] (s : Set α) : IsLUB s (sSup s)
• IsLUB.sSup_eq 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} : IsLUB s a → sSup s = a
• isLUB_iff_sSup_eq 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} : IsLUB s a ↔ sSup s = a
• CompleteLattice.mk 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_4} [toLattice : Lattice α] [toSupSet : SupSet α] (isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)) [toInfSet : InfSet α] (isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)) [toBoundedOrder : BoundedOrder α] : CompleteLattice α
• isLUB_iSup 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} : IsLUB (Set.range f) (⨆ j, f j)
• IsLUB.iSup_eq 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} {a : α} (h : IsLUB (Set.range f) a) : ⨆ j, f j = a
• isLUB_biSup 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [CompleteLattice α] {s : Set β} {f : β → α} : IsLUB (f '' s) (⨆ x ∈ s, f x)
• GaloisConnection.isLUB_u 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) {a : α} : IsLUB {b | l b ≤ a} (u a)
• GaloisCoinsertion.isLUB_of_l_image 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {u : α → β} {l : β → α} [Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) {s : Set β} {a : α} (hs : IsLUB (l '' s) a) : IsLUB s (u a)
• GaloisConnection.isLUB_l_image 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {s : Set α} {a : α} (h : IsLUB s a) : IsLUB (l '' s) (l a)
• GaloisInsertion.isLUB_of_u_image 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {l : α → β} {u : β → α} [Preorder α] [Preorder β] (gi : GaloisInsertion l u) {s : Set β} {a : α} (hs : IsLUB (u '' s) a) : IsLUB s (l a)
• isLUB_image2_of_isLUB_isLUB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) (ha₀ : IsLUB s a₀) (hb₀ : IsLUB t b₀) : IsLUB (Set.image2 l s t) (l a₀ b₀)
• isGLB_image2_of_isGLB_isLUB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (u₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ u₂ a) (u a ∘ ⇑OrderDual.ofDual)) (ha₀ : IsGLB s a₀) (hb₀ : IsLUB t b₀) : IsGLB (Set.image2 u s t) (u a₀ b₀)
• isGLB_image2_of_isLUB_isGLB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ u₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (u₂ a) (u a)) (ha₀ : IsLUB s a₀) (hb₀ : IsGLB t b₀) : IsGLB (Set.image2 u s t) (u a₀ b₀)
• isLUB_image2_of_isGLB_isLUB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) (ha₀ : IsGLB s a₀) (hb₀ : IsLUB t b₀) : IsLUB (Set.image2 l s t) (l a₀ b₀)
• isLUB_image2_of_isLUB_isGLB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) (ha₀ : IsLUB s a₀) (hb₀ : IsGLB t b₀) : IsLUB (Set.image2 l s t) (l a₀ b₀)
• isGLB_image2_of_isLUB_isLUB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ u₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ u₂ a) (u a ∘ ⇑OrderDual.ofDual)) (ha₀ : IsLUB s a₀) (hb₀ : IsLUB t b₀) : IsGLB (Set.image2 u s t) (u a₀ b₀)
• isLUB_image2_of_isGLB_isGLB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) (ha₀ : IsGLB s a₀) (hb₀ : IsGLB t b₀) : IsLUB (Set.image2 l s t) (l a₀ b₀)
• conditionallyCompleteLatticeOfLatticeOfsSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Defs
  (α : Type u_2) [H1 : Lattice α] [SupSet α] (isLUB_sSup : ∀ (s : Set α), BddAbove s → s.Nonempty → IsLUB s (sSup s)) : ConditionallyCompleteLattice α
• ConditionallyCompleteLattice.isLUB_csSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Defs
  {α : Type u_2} [self : ConditionallyCompleteLattice α] (s : Set α) : s.Nonempty → BddAbove s → IsLUB s (sSup s)
• ConditionallyCompleteLattice.mk 📋 Mathlib.Order.ConditionallyCompleteLattice.Defs
  {α : Type u_2} [toLattice : Lattice α] [toSupSet : SupSet α] [toInfSet : InfSet α] (isLUB_csSup : ∀ (s : Set α), s.Nonempty → BddAbove s → IsLUB s (sSup s)) (isGLB_csInf : ∀ (s : Set α), s.Nonempty → BddBelow s → IsGLB s (sInf s)) : ConditionallyCompleteLattice α
• conditionallyCompleteLatticeOfsSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Defs
  (α : Type u_2) [H1 : PartialOrder α] [H2 : SupSet α] (bddAbove_pair : ∀ (a b : α), BddAbove {a, b}) (bddBelow_pair : ∀ (a b : α), BddBelow {a, b}) (isLUB_sSup : ∀ (s : Set α), BddAbove s → s.Nonempty → IsLUB s (sSup s)) : ConditionallyCompleteLattice α
• ConditionallyCompletePartialOrderSup.mk 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Defs
  {α : Type u_3} [toPartialOrder : PartialOrder α] [toSupSet : SupSet α] (isLUB_csSup_of_directed : ∀ (s : Set α), DirectedOn (fun x1 x2 => x1 ≤ x2) s → s.Nonempty → BddAbove s → IsLUB s (sSup s)) : ConditionallyCompletePartialOrderSup α
• ConditionallyCompletePartialOrderSup.isLUB_csSup_of_directed 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Defs
  {α : Type u_3} [self : ConditionallyCompletePartialOrderSup α] (s : Set α) : DirectedOn (fun x1 x2 => x1 ≤ x2) s → s.Nonempty → BddAbove s → IsLUB s (sSup s)
• DirectedOn.isLUB_csSup 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Defs
  {α : Type u_2} [ConditionallyCompletePartialOrderSup α] {s : Set α} (h_dir : DirectedOn (fun x1 x2 => x1 ≤ x2) s) (h_non : s.Nonempty) (h_bdd : BddAbove s) : IsLUB s (sSup s)
• IsLUB.csSup_eq 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsLUB s a) (ne : s.Nonempty) : sSup s = a
• isLUB_csSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (hn : s.Nonempty) (hb : BddAbove s := by bddDefault) : IsLUB s (sSup s)
• WithTop.isLUB_sSup' 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {β : Type u_5} [ConditionallyCompleteLattice β] {s : Set (WithTop β)} (hs : s.Nonempty) : IsLUB s (sSup s)
• isLUB_csSup' 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} (hs : BddAbove s) : IsLUB s (sSup s)
• WithTop.isLUB_sSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] (s : Set (WithTop α)) : IsLUB s (sSup s)
• WithBot.isLUB_sSup' 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {β : Type u_5} [ConditionallyCompleteLattice β] {s : Set (WithBot β)} (hs : BddAbove s) : IsLUB s (sSup s)
• Finset.isLUB_sup' 📋 Mathlib.Data.Finset.Lattice.Fold
  {α : Type u_2} [SemilatticeSup α] {s : Finset α} (hs : s.Nonempty) : IsLUB (↑s) (s.sup' hs id)
• Finset.isLUB_sup_id 📋 Mathlib.Data.Finset.Lattice.Fold
  {α : Type u_2} [SemilatticeSup α] [OrderBot α] {s : Finset α} : IsLUB (↑s) (s.sup id)
• Finset.isLUB_sup 📋 Mathlib.Data.Finset.Lattice.Fold
  {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} : IsLUB (f '' ↑s) (s.sup f)
• Finset.isLUB_mem 📋 Mathlib.Data.Finset.Max
  {α : Type u_1} [LinearOrder α] {i : α} (s : Finset α) (his : IsLUB (↑s) i) (hs : s.Nonempty) : i ∈ s
• Finset.isLUB_iff_isGreatest 📋 Mathlib.Data.Finset.Max
  {α : Type u_1} [LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) : IsLUB (↑s) i ↔ IsGreatest (↑s) i
• Directed.isLUB_ciSup 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
  {α : Type u_1} {ι : Sort u_4} [ConditionallyCompletePartialOrderSup α] [Nonempty ι] {f : ι → α} (hd : Directed (fun x1 x2 => x1 ≤ x2) f) (H : BddAbove (Set.range f)) : IsLUB (Set.range f) (⨆ i, f i)
• DirectedOn.isLUB_ciSup_set 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
  {α : Type u_1} {β : Type u_2} [ConditionallyCompletePartialOrderSup α] {f : β → α} {s : Set β} (hd : DirectedOn (fun x1 x2 => x1 ≤ x2) (f '' s)) (H : BddAbove (f '' s)) (Hne : s.Nonempty) : IsLUB (f '' s) (⨆ i, f ↑i)
• IsLUB.ciSup_eq 📋 Mathlib.Order.ConditionallyCompleteLattice.Indexed
  {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] {a : α} [Nonempty ι] {f : ι → α} (H : IsLUB (Set.range f) a) : ⨆ i, f i = a
• isLUB_ciSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Indexed
  {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLattice α] [Nonempty ι] {f : ι → α} (H : BddAbove (Set.range f)) : IsLUB (Set.range f) (⨆ i, f i)
• IsLUB.ciSup_set_eq 📋 Mathlib.Order.ConditionallyCompleteLattice.Indexed
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {a : α} {s : Set β} {f : β → α} (H : IsLUB (f '' s) a) (Hne : s.Nonempty) : ⨆ i, f ↑i = a
• isLUB_ciSup_set 📋 Mathlib.Order.ConditionallyCompleteLattice.Indexed
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : β → α} {s : Set β} (H : BddAbove (f '' s)) (Hne : s.Nonempty) : IsLUB (f '' s) (⨆ i, f ↑i)
• IsLUB.isSuccPrelimit_of_notMem 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsLUB s a) (ha : a ∉ s) : Order.IsSuccPrelimit a
• IsLUB.mem_of_not_isSuccPrelimit 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsLUB s a) (ha : ¬Order.IsSuccPrelimit a) : a ∈ s
• Order.IsSuccLimit.isLUB_Iio 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [LinearOrder α] (ha : Order.IsSuccLimit a) : IsLUB (Set.Iio a) a
• IsLUB.isSuccLimit_of_notMem 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) (ha : a ∉ s) : Order.IsSuccLimit a
• IsLUB.mem_of_not_isSuccLimit 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) (ha : ¬Order.IsSuccLimit a) : a ∈ s
• Order.IsSuccPrelimit.isLUB_Iio 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [LinearOrder α] (ha : Order.IsSuccPrelimit a) : IsLUB (Set.Iio a) a
• Order.isLUB_Iio_iff_isSuccPrelimit 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [LinearOrder α] : IsLUB (Set.Iio a) a ↔ Order.IsSuccPrelimit a
• IsLUB.mem_of_nonempty_of_not_isSuccLimit 📋 Mathlib.Order.SuccPred.CompleteLinearOrder
  {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} {x : α} (hs : IsLUB s x) (hne : s.Nonempty) (hx : ¬Order.IsSuccLimit x) : x ∈ s
• IsLUB.mem_of_nonempty_of_not_isSuccPrelimit 📋 Mathlib.Order.SuccPred.CompleteLinearOrder
  {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} {x : α} (hs : IsLUB s x) (hne : s.Nonempty) (hx : ¬Order.IsSuccPrelimit x) : x ∈ s
• IsLUB.exists_of_nonempty_of_not_isSuccLimit 📋 Mathlib.Order.SuccPred.CompleteLinearOrder
  {ι : Sort u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] [Nonempty ι] {f : ι → α} {x : α} (hf : IsLUB (Set.range f) x) (hx : ¬Order.IsSuccLimit x) : ∃ i, f i = x
• IsLUB.exists_of_nonempty_of_not_isSuccPrelimit 📋 Mathlib.Order.SuccPred.CompleteLinearOrder
  {ι : Sort u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] [Nonempty ι] {f : ι → α} {x : α} (hf : IsLUB (Set.range f) x) (hx : ¬Order.IsSuccPrelimit x) : ∃ i, f i = x
• OmegaCompletePartialOrder.isLUB_range_ωSup 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} [OmegaCompletePartialOrder α] (c : OmegaCompletePartialOrder.Chain α) : IsLUB (Set.range ⇑c) (OmegaCompletePartialOrder.ωSup c)
• OmegaCompletePartialOrder.ωSup_eq_of_isLUB 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} [OmegaCompletePartialOrder α] {c : OmegaCompletePartialOrder.Chain α} {a : α} (h : IsLUB (Set.range ⇑c) a) : a = OmegaCompletePartialOrder.ωSup c
• OmegaCompletePartialOrder.ωScottContinuous.isLUB 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α → β} {c : OmegaCompletePartialOrder.Chain α} (hf : OmegaCompletePartialOrder.ωScottContinuous f) : IsLUB (Set.range ⇑(c.map { toFun := f, monotone' := ⋯ })) (f (OmegaCompletePartialOrder.ωSup c))
• isLUB_atoms_le 📋 Mathlib.Order.Atoms
  {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomistic α] (b : α) : IsLUB {a | IsAtom a ∧ a ≤ b} b
• IsAtomistic.isLUB_atoms 📋 Mathlib.Order.Atoms
  {α : Type u_2} {inst✝ : PartialOrder α} {inst✝¹ : OrderBot α} [self : IsAtomistic α] (b : α) : ∃ s, IsLUB s b ∧ ∀ a ∈ s, IsAtom a
• IsAtomistic.mk 📋 Mathlib.Order.Atoms
  {α : Type u_2} [PartialOrder α] [OrderBot α] (isLUB_atoms : ∀ (b : α), ∃ s, IsLUB s b ∧ ∀ a ∈ s, IsAtom a) : IsAtomistic α
• isAtomistic_iff 📋 Mathlib.Order.Atoms
  (α : Type u_2) [PartialOrder α] [OrderBot α] : IsAtomistic α ↔ ∀ (b : α), ∃ s, IsLUB s b ∧ ∀ a ∈ s, IsAtom a
• isLUB_atoms_top 📋 Mathlib.Order.Atoms
  {α : Type u_2} [PartialOrder α] [OrderBot α] [IsAtomistic α] [OrderTop α] : IsLUB {a | IsAtom a} ⊤
• SemilatticeSup.toCompleteSemilatticeSup 📋 Mathlib.Order.SupClosed
  {α : Type u_3} [SemilatticeSup α] (sSup : Set α → α) (h : ∀ (s : Set α), SupClosed s → IsLUB s (sSup s)) : CompleteSemilatticeSup α
• isLUB_supClosure 📋 Mathlib.Order.SupClosed
  {α : Type u_3} [SemilatticeSup α] {s : Set α} {a : α} : IsLUB (supClosure s) a ↔ IsLUB s a
• Filter.isLUB_sSup 📋 Mathlib.Order.Filter.Basic
  {α : Type u} (s : Set (Filter α)) : IsLUB s (sSup s)
• IsLUB.biUnion_Iic_eq_Iic 📋 Mathlib.Order.Interval.Set.Disjoint
  {α : Type v} [Preorder α] {s : Set α} {a : α} (a_lub : IsLUB s a) (a_mem : a ∈ s) : ⋃ x ∈ s, Set.Iic x = Set.Iic a
• IsLUB.iUnion_Iio_eq 📋 Mathlib.Order.Interval.Set.Disjoint
  {ι : Sort u} {α : Type v} [LinearOrder α] {a : α} {f : ι → α} (h : IsLUB (Set.range f) a) : ⋃ x, Set.Iio (f x) = Set.Iio a
• IsLUB.biUnion_Iio_eq 📋 Mathlib.Order.Interval.Set.Disjoint
  {α : Type v} [LinearOrder α] {s : Set α} {a : α} (h : IsLUB s a) : ⋃ x ∈ s, Set.Iio x = Set.Iio a
• IsLUB.biUnion_Iic_eq_Iio 📋 Mathlib.Order.Interval.Set.Disjoint
  {α : Type v} [LinearOrder α] {s : Set α} {a : α} (a_lub : IsLUB s a) (a_notMem : a ∉ s) : ⋃ x ∈ s, Set.Iic x = Set.Iio a
• dirSupClosed_iff_of_linearOrder 📋 Mathlib.Order.DirSupClosed
  {α : Type u_1} {s : Set α} [LinearOrder α] : DirSupClosed s ↔ ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
• dirSupInacc_iff_of_linearOrder 📋 Mathlib.Order.DirSupClosed
  {α : Type u_1} {s : Set α} [LinearOrder α] : DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty
• DirSupInacc.of_inter_subset 📋 Mathlib.Order.DirSupClosed
  {α : Type u_1} {s : Set α} [Preorder α] (h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Set.Ici b ∩ d ⊆ s) : DirSupInacc s
• dirSupInacc_iff_inter_subset 📋 Mathlib.Order.DirSupClosed
  {α : Type u_1} {s : Set α} [Preorder α] : DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Set.Ici b ∩ d ⊆ s
• dirSupClosedOn_iff_of_linearOrder 📋 Mathlib.Order.DirSupClosed
  {α : Type u_1} {s : Set α} {D : Set (Set α)} [LinearOrder α] : DirSupClosedOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
• dirSupInaccOn_iff_of_linearOrder 📋 Mathlib.Order.DirSupClosed
  {α : Type u_1} {s : Set α} {D : Set (Set α)} [LinearOrder α] : DirSupInaccOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty
• DirSupInaccOn.of_inter_subset 📋 Mathlib.Order.DirSupClosed
  {α : Type u_1} {s : Set α} {D : Set (Set α)} [Preorder α] (h : ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Set.Ici b ∩ d ⊆ s) : DirSupInaccOn D s
• dirSupInaccOn_iff_inter_subset 📋 Mathlib.Order.DirSupClosed
  {α : Type u_1} {s : Set α} {D : Set (Set α)} [Preorder α] (hDL : IsLowerSet D) : DirSupInaccOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Set.Ici b ∩ d ⊆ s
• Order.IsNormal.map_isLUB 📋 Mathlib.Order.IsNormal
  {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} [LinearOrder α] [LinearOrder β] (hf : Order.IsNormal f) {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) : IsLUB (f '' s) (f a)
• Order.IsNormal.isLUB_image_Iio_of_isSuccLimit 📋 Mathlib.Order.IsNormal
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : Order.IsNormal f) {a : α} (ha : Order.IsSuccLimit a) : IsLUB (f '' Set.Iio a) (f a)
• Order.IsNormal.of_succ_lt 📋 Mathlib.Order.IsNormal
  {α : Type u_1} {β : Type u_2} {f : α → β} [LinearOrder α] [WellFoundedLT α] [SuccOrder α] [LinearOrder β] (hs : ∀ (a : α), f a < f (Order.succ a)) (hl : ∀ {a : α}, Order.IsSuccLimit a → IsLUB (f '' Set.Iio a) (f a)) : Order.IsNormal f
• IsMaxOn.isLUB 📋 Mathlib.Order.Filter.Extr
  {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} (ha : a ∈ s) (hfsa : IsMaxOn f s a) : IsLUB {x | ∃ x_1 ∈ s, f x_1 = x} (f a)
• IsLUB.range_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {f : β → α} {a : α} {F : Filter β} [F.NeBot] (hle : ∀ (i : β), f i ≤ a) (hlim : Filter.Tendsto f F (nhds a)) : IsLUB (Set.range f) a
• Preorder.colimitCoconeOfIsLUB 📋 Mathlib.CategoryTheory.Limits.Preorder
  {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) {pt : C} (h : IsLUB (Set.range F.obj) pt) : CategoryTheory.Limits.ColimitCocone F
• Preorder.hasColimit_iff_hasLUB 📋 Mathlib.CategoryTheory.Limits.Preorder
  {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.HasColimit F ↔ ∃ x, IsLUB (Set.range F.obj) x
• Preorder.isColimitOfIsLUB 📋 Mathlib.CategoryTheory.Limits.Preorder
  {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cocone F) (h : IsLUB (Set.range F.obj) c.pt) : CategoryTheory.Limits.IsColimit c
• Preorder.isLUB_of_isColimit 📋 Mathlib.CategoryTheory.Limits.Preorder
  {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) {c : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit c) : IsLUB (Set.range F.obj) c.pt
• Preorder.colimitCoconeOfIsLUB_cocone 📋 Mathlib.CategoryTheory.Limits.Preorder
  {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) {pt : C} (h : IsLUB (Set.range F.obj) pt) : (Preorder.colimitCoconeOfIsLUB F h).cocone = Preorder.coconeOfUpperBound F ⋯
• Preorder.colimitCoconeOfIsLUB_isColimit 📋 Mathlib.CategoryTheory.Limits.Preorder
  {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) {pt : C} (h : IsLUB (Set.range F.obj) pt) : (Preorder.colimitCoconeOfIsLUB F h).isColimit = Preorder.isColimitOfIsLUB F (Preorder.coconeOfUpperBound F ⋯) h
• IsGLB.inv 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G} (h : IsGLB s a) : IsLUB s⁻¹ a⁻¹
• IsGLB.neg 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G} (h : IsGLB s a) : IsLUB (-s) (-a)
• IsLUB.inv 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G} (h : IsLUB s a) : IsGLB s⁻¹ a⁻¹
• IsLUB.neg 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G} (h : IsLUB s a) : IsGLB (-s) (-a)
• isGLB_inv 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G} : IsGLB s⁻¹ a ↔ IsLUB s a⁻¹
• isGLB_inv' 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G} : IsGLB s⁻¹ a⁻¹ ↔ IsLUB s a
• isGLB_neg 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G} : IsGLB (-s) a ↔ IsLUB s (-a)
• isGLB_neg' 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G} : IsGLB (-s) (-a) ↔ IsLUB s a
• isLUB_inv 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G} : IsLUB s⁻¹ a ↔ IsGLB s a⁻¹
• isLUB_inv' 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G} : IsLUB s⁻¹ a⁻¹ ↔ IsGLB s a
• isLUB_neg 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G} : IsLUB (-s) a ↔ IsGLB s (-a)
• isLUB_neg' 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G} : IsLUB (-s) (-a) ↔ IsGLB s a
• IsGLB.div 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s t : Set G} {a b : G} (hs : IsGLB s a) (ht : IsLUB t b) : IsGLB (s / t) (a / b)
• IsGLB.sub 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s t : Set G} {a b : G} (hs : IsGLB s a) (ht : IsLUB t b) : IsGLB (s - t) (a - b)
• IsLUB.div 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s t : Set G} {a b : G} (hs : IsLUB s a) (ht : IsGLB t b) : IsLUB (s / t) (a / b)
• IsLUB.sub 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s t : Set G} {a b : G} (hs : IsLUB s a) (ht : IsGLB t b) : IsLUB (s - t) (a - b)
• IsLUB.add 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [AddGroup G] [Preorder G] [AddLeftMono G] [AddRightMono G] {s t : Set G} {a b : G} (hs : IsLUB s a) (ht : IsLUB t b) : IsLUB (s + t) (a + b)
• IsLUB.mul 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {G : Type u_2} [Group G] [Preorder G] [MulLeftMono G] [MulRightMono G] {s t : Set G} {a b : G} (hs : IsLUB s a) (ht : IsLUB t b) : IsLUB (s * t) (a * b)
• Real.exists_isLUB 📋 Mathlib.Algebra.Order.Archimedean.Real.Basic
  {s : Set ℝ} (hne : s.Nonempty) (hbdd : BddAbove s) : ∃ x, IsLUB s x
• Real.isLUB_sSup 📋 Mathlib.Algebra.Order.Archimedean.Real.Basic
  {s : Set ℝ} (h₁ : s.Nonempty) (h₂ : BddAbove s) : IsLUB s (sSup s)
• Real.sSup_def 📋 Mathlib.Algebra.Order.Archimedean.Real.Basic
  (s : Set ℝ) : sSup s = if h : s.Nonempty ∧ BddAbove s then Classical.choose ⋯ else 0
• Dense.isLUB_inter_iff 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_3} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {s t : Set α} (hs : Dense s) (ht : IsOpen t) {x : α} : IsLUB (t ∩ s) x ↔ IsLUB t x
• isLUB_iff_of_subset_of_subset_closure 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_3} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {s t : Set α} (hst : s ⊆ t) (hts : t ⊆ closure s) {x : α} : IsLUB s x ↔ IsLUB t x
• IsLUB.nhdsWithin_neBot 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : (nhdsWithin a s).NeBot
• IsLUB.mem_closure 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : a ∈ closure s
• IsClosed.isLUB_mem 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) (sc : IsClosed s) : a ∈ s
• IsLUB.mem_of_isClosed 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) (sc : IsClosed s) : a ∈ s
• IsLUB.frequently_nhds_mem 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : ∃ᶠ (x : α) in nhds a, x ∈ s
• IsLUB.frequently_mem 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : ∃ᶠ (x : α) in nhdsWithin a (Set.Iic a), x ∈ s
• isLUB_of_mem_closure 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {s : Set α} {a : α} (hsa : a ∈ upperBounds s) (hsf : a ∈ closure s) : IsLUB s a
• isLUB_of_mem_nhds 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {s : Set α} {a : α} {f : Filter α} (hsa : a ∈ upperBounds s) (hsf : s ∈ f) [(f ⊓ nhds a).NeBot] : IsLUB s a
• IsGLB.isLUB_of_tendsto 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : AntitoneOn f s) (ha : IsGLB s a) (hs : s.Nonempty) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : IsLUB (f '' s) b
• IsLUB.isGLB_of_tendsto 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : AntitoneOn f s) (ha : IsLUB s a) (hs : s.Nonempty) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : IsGLB (f '' s) b
• IsLUB.isLUB_of_tendsto 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsLUB s a) (hs : s.Nonempty) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : IsLUB (f '' s) b
• IsLUB.mem_lowerBounds_of_tendsto 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : AntitoneOn f s) (ha : IsLUB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : b ∈ lowerBounds (f '' s)
• IsLUB.mem_upperBounds_of_tendsto 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) (ha : IsLUB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : b ∈ upperBounds (f '' s)
• IsLUB.exists_seq_monotone_tendsto 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {t : Set α} {x : α} [(nhds x).IsCountablyGenerated] (htx : IsLUB t x) (ht : t.Nonempty) : ∃ u, Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Filter.Tendsto u Filter.atTop (nhds x) ∧ ∀ (n : ℕ), u n ∈ t
• IsLUB.exists_seq_strictMono_tendsto_of_notMem 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {t : Set α} {x : α} [(nhds x).IsCountablyGenerated] (htx : IsLUB t x) (notMem : x ∉ t) (ht : t.Nonempty) : ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Filter.Tendsto u Filter.atTop (nhds x) ∧ ∀ (n : ℕ), u n ∈ t
• IsCompact.isLUB_sSup 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIciTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : IsLUB s (sSup s)
• IsCompact.exists_isLUB 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [ClosedIciTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : ∃ x ∈ s, IsLUB s x
• tendsto_atBot_isLUB 📋 Mathlib.Topology.Order.MonotoneConvergence
  {α : Type u_1} {ι : Type u_3} [Preorder ι] [TopologicalSpace α] [Preorder α] [SupConvergenceClass α] {f : ι → α} {a : α} (h_anti : Antitone f) (ha : IsLUB (Set.range f) a) : Filter.Tendsto f Filter.atBot (nhds a)
• tendsto_atTop_isLUB 📋 Mathlib.Topology.Order.MonotoneConvergence
  {α : Type u_1} {ι : Type u_3} [Preorder ι] [TopologicalSpace α] [Preorder α] [SupConvergenceClass α] {f : ι → α} {a : α} (h_mono : Monotone f) (ha : IsLUB (Set.range f) a) : Filter.Tendsto f Filter.atTop (nhds a)
• isLUB_of_tendsto_atBot 📋 Mathlib.Topology.Order.MonotoneConvergence
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [Preorder β] [IsCodirectedOrder β] [Nonempty β] {f : β → α} {a : α} (hf : Antitone f) (ha : Filter.Tendsto f Filter.atBot (nhds a)) : IsLUB (Set.range f) a
• isLUB_of_tendsto_atTop 📋 Mathlib.Topology.Order.MonotoneConvergence
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [Preorder β] [IsDirectedOrder β] [Nonempty β] {f : β → α} {a : α} (hf : Monotone f) (ha : Filter.Tendsto f Filter.atTop (nhds a)) : IsLUB (Set.range f) a
• SupConvergenceClass.mk 📋 Mathlib.Topology.Order.MonotoneConvergence
  {α : Type u_3} [Preorder α] [TopologicalSpace α] (tendsto_coe_atTop_isLUB : ∀ (a : α) (s : Set α), IsLUB s a → Filter.Tendsto Subtype.val Filter.atTop (nhds a)) : SupConvergenceClass α
• SupConvergenceClass.tendsto_coe_atTop_isLUB 📋 Mathlib.Topology.Order.MonotoneConvergence
  {α : Type u_3} {inst✝ : Preorder α} {inst✝¹ : TopologicalSpace α} [self : SupConvergenceClass α] (a : α) (s : Set α) : IsLUB s a → Filter.Tendsto Subtype.val Filter.atTop (nhds a)
• isLUB_hasProd' 📋 Mathlib.Topology.Algebra.InfiniteSum.Order
  {ι : Type u_1} {α : Type u_3} [CommMonoid α] [PartialOrder α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (hf : HasProd f a) : IsLUB (Set.range fun s => ∏ i ∈ s, f i) a
• isLUB_hasSum' 📋 Mathlib.Topology.Algebra.InfiniteSum.Order
  {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (hf : HasSum f a) : IsLUB (Set.range fun s => ∑ i ∈ s, f i) a
• isLUB_hasProd 📋 Mathlib.Topology.Algebra.InfiniteSum.Order
  {ι : Type u_1} {α : Type u_3} [CommMonoid α] [Preorder α] [IsOrderedMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (h : ∀ (i : ι), 1 ≤ f i) (hf : HasProd f a) : IsLUB (Set.range fun s => ∏ i ∈ s, f i) a
• isLUB_hasSum 📋 Mathlib.Topology.Algebra.InfiniteSum.Order
  {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] [TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} (h : ∀ (i : ι), 0 ≤ f i) (hf : HasSum f a) : IsLUB (Set.range fun s => ∑ i ∈ s, f i) a
• hasProd_of_isLUB 📋 Mathlib.Topology.Algebra.InfiniteSum.Order
  {ι : Type u_1} {α : Type u_3} [CommMonoid α] [LinearOrder α] [CanonicallyOrderedMul α] [TopologicalSpace α] [OrderTopology α] {f : ι → α} (b : α) (hf : IsLUB (Set.range fun s => ∏ i ∈ s, f i) b) : HasProd f b

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c