Loogle!

Result

Found 124 declarations mentioning lowerBounds.

• lowerBounds 📋 Mathlib.Order.Bounds.Defs
  {α : Type u_1} [LE α] (s : Set α) : Set α
• lowerBounds_empty 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] : lowerBounds ∅ = Set.univ
• Set.Nonempty.bddAbove_lowerBounds 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} (hs : s.Nonempty) : BddAbove (lowerBounds s)
• lowerBounds_Ici 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a : α} : lowerBounds (Set.Ici a) = Set.Iic a
• subset_lowerBounds_upperBounds 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] (s : Set α) : s ⊆ lowerBounds (upperBounds s)
• subset_upperBounds_lowerBounds 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] (s : Set α) : s ⊆ upperBounds (lowerBounds s)
• lowerBounds_singleton 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a : α} : lowerBounds {a} = Set.Iic a
• NoBotOrder.lowerBounds_univ 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] [NoBotOrder α] : lowerBounds Set.univ = ∅
• mem_lowerBounds_univ 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a : α} : a ∈ lowerBounds Set.univ ↔ IsBot a
• isLUB_lowerBounds 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsLUB (lowerBounds s) a ↔ IsGLB s a
• IsGLB.lowerBounds_eq 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsGLB s a) : lowerBounds s = Set.Iic a
• IsLeast.lowerBounds_eq 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLeast s a) : lowerBounds s = Set.Iic a
• lowerBounds_Icc 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a b : α} (h : b ≤ a) : lowerBounds (Set.Icc b a) = Set.Iic b
• lowerBounds_Ico 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a b : α} (h : b < a) : lowerBounds (Set.Ico b a) = Set.Iic b
• bot_mem_lowerBounds 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] [OrderBot α] (s : Set α) : ⊥ ∈ lowerBounds s
• mem_lowerBounds_iff_subset_Ici 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} : a ∈ lowerBounds s ↔ s ⊆ Set.Ici a
• lowerBounds_mono_of_isCoinitialFor 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s t : Set α} (hst : IsCoinitialFor s t) : lowerBounds t ⊆ lowerBounds s
• lowerBounds_mono_set 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] ⦃s t : Set α⦄ (hst : s ⊆ t) : lowerBounds t ⊆ lowerBounds s
• le_isGLB_iff 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (h : IsGLB s a) : b ≤ a ↔ b ∈ lowerBounds s
• isGLB_iff_le_iff 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsGLB s a ↔ ∀ (b : α), b ≤ a ↔ b ∈ lowerBounds s
• mem_lowerBounds 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} : a ∈ lowerBounds s ↔ ∀ x ∈ s, a ≤ x
• lowerBounds_insert 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] (a : α) (s : Set α) : lowerBounds (insert a s) = Set.Iic a ∩ lowerBounds s
• isGLB_congr 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s t : Set α} {a : α} (h : lowerBounds s = lowerBounds t) : IsGLB s a ↔ IsGLB t a
• OrderBot.lowerBounds_univ 📋 Mathlib.Order.Bounds.Basic
  {γ : Type u_3} [PartialOrder γ] [OrderBot γ] : lowerBounds Set.univ = {⊥}
• lowerBounds_union 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s t : Set α} : lowerBounds (s ∪ t) = lowerBounds s ∩ lowerBounds t
• lowerBounds_mono_mem 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} ⦃a b : α⦄ (hab : b ≤ a) : a ∈ lowerBounds s → b ∈ lowerBounds s
• union_lowerBounds_subset_lowerBounds_inter 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s t : Set α} : lowerBounds s ∪ lowerBounds t ⊆ lowerBounds (s ∩ t)
• lowerBounds_le_upperBounds 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds s) : s.Nonempty → a ≤ b
• lt_isGLB_iff 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a b : α} (ha : IsGLB s a) : b < a ↔ ∃ c ∈ lowerBounds s, b < c
• lowerBounds_mono 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] ⦃s t : Set α⦄ (hst : s ⊆ t) ⦃a b : α⦄ (hab : b ≤ a) : a ∈ lowerBounds t → b ∈ lowerBounds s
• lowerBounds_le_upperBounds_of_nonempty_inter 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s s' : Set α} {a b : α} (h : (s ∩ s').Nonempty) (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds s') : a ≤ b
• lowerBounds_Ioc 📋 Mathlib.Order.Bounds.Basic
  {γ : Type u_3} [SemilatticeSup γ] [DenselyOrdered γ] {a b : γ} (hab : a < b) : lowerBounds (Set.Ioc a b) = Set.Iic a
• lowerBounds_Ioo 📋 Mathlib.Order.Bounds.Basic
  {γ : Type u_3} [SemilatticeSup γ] [DenselyOrdered γ] {a b : γ} (hab : a < b) : lowerBounds (Set.Ioo a b) = Set.Iic a
• isLeast_union_iff 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a : α} {s t : Set α} : IsLeast (s ∪ t) a ↔ IsLeast s a ∧ a ∈ lowerBounds t ∨ a ∈ lowerBounds s ∧ IsLeast t a
• lowerBounds_Ioi 📋 Mathlib.Order.Bounds.Basic
  {γ : Type u_3} [LinearOrder γ] [DenselyOrdered γ] {a : γ} : lowerBounds (Set.Ioi a) = Set.Iic a
• lowerBounds_prod 📋 Mathlib.Order.Bounds.Basic
  {α : 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
• Antitone.image_lowerBounds_subset_upperBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {s : Set α} : f '' lowerBounds s ⊆ upperBounds (f '' s)
• Antitone.image_upperBounds_subset_lowerBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {s : Set α} : f '' upperBounds s ⊆ lowerBounds (f '' s)
• Monotone.image_lowerBounds_subset_lowerBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {s : Set α} : f '' lowerBounds s ⊆ lowerBounds (f '' s)
• Antitone.mem_lowerBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {a : α} {s : Set α} : a ∈ upperBounds s → f a ∈ lowerBounds (f '' s)
• Antitone.mem_upperBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {a : α} {s : Set α} : a ∈ lowerBounds s → f a ∈ upperBounds (f '' s)
• Monotone.mem_lowerBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {a : α} {s : Set α} (Ha : a ∈ lowerBounds s) : f a ∈ lowerBounds (f '' s)
• AntitoneOn.map_bddBelow 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) : (lowerBounds s ∩ t).Nonempty → BddAbove (f '' s)
• MonotoneOn.map_bddBelow 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) : (lowerBounds s ∩ t).Nonempty → BddBelow (f '' s)
• AntitoneOn.image_lowerBounds_subset_upperBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) : f '' (lowerBounds s ∩ t) ⊆ upperBounds (f '' s)
• AntitoneOn.image_upperBounds_subset_lowerBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) : f '' (upperBounds s ∩ t) ⊆ lowerBounds (f '' s)
• AntitoneOn.mem_lowerBounds_image_self 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : AntitoneOn f t) : a ∈ upperBounds t → a ∈ t → f a ∈ lowerBounds (f '' t)
• AntitoneOn.mem_upperBounds_image_self 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : AntitoneOn f t) : a ∈ lowerBounds t → a ∈ t → f a ∈ upperBounds (f '' t)
• MonotoneOn.image_lowerBounds_subset_lowerBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) : f '' (lowerBounds s ∩ t) ⊆ lowerBounds (f '' s)
• MonotoneOn.mem_lowerBounds_image_self 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : MonotoneOn f t) : a ∈ lowerBounds t → a ∈ t → f a ∈ lowerBounds (f '' t)
• AntitoneOn.mem_lowerBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} {a : α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) (Has : a ∈ upperBounds s) : a ∈ t → f a ∈ lowerBounds (f '' s)
• AntitoneOn.mem_upperBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} {a : α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) (Has : a ∈ lowerBounds s) : a ∈ t → f a ∈ upperBounds (f '' s)
• MonotoneOn.mem_lowerBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} {a : α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) (Has : a ∈ lowerBounds s) (Hat : a ∈ t) : f a ∈ lowerBounds (f '' s)
• StrictAnti.mem_lowerBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {a : α} {s : Set α} (hf : StrictAnti f) : f a ∈ lowerBounds (f '' s) ↔ a ∈ upperBounds s
• StrictAnti.mem_upperBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {a : α} {s : Set α} (hf : StrictAnti f) : f a ∈ upperBounds (f '' s) ↔ a ∈ lowerBounds s
• StrictMono.mem_lowerBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {a : α} {s : Set α} (hf : StrictMono f) : f a ∈ lowerBounds (f '' s) ↔ a ∈ lowerBounds s
• image2_lowerBounds_lowerBounds_subset 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : Set.image2 f (lowerBounds s) (lowerBounds t) ⊆ lowerBounds (Set.image2 f s t)
• image2_lowerBounds_lowerBounds_subset_lowerBounds_image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : Set.image2 f (upperBounds s) (upperBounds t) ⊆ lowerBounds (Set.image2 f s t)
• image2_lowerBounds_upperBounds_subset_lowerBounds_image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : Set.image2 f (lowerBounds s) (upperBounds t) ⊆ lowerBounds (Set.image2 f s t)
• image2_lowerBounds_upperBounds_subset_upperBounds_image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : Set.image2 f (lowerBounds s) (upperBounds t) ⊆ upperBounds (Set.image2 f s t)
• image2_upperBounds_lowerBounds_subset_lowerBounds_image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : Set.image2 f (upperBounds s) (lowerBounds t) ⊆ lowerBounds (Set.image2 f s t)
• image2_upperBounds_lowerBounds_subset_upperBounds_image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : Set.image2 f (upperBounds s) (lowerBounds t) ⊆ upperBounds (Set.image2 f s t)
• image2_upperBounds_upperBounds_subset_upperBounds_image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : Set.image2 f (lowerBounds s) (lowerBounds t) ⊆ upperBounds (Set.image2 f s t)
• mem_lowerBounds_image2 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ lowerBounds (Set.image2 f s t)
• mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a ∈ upperBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ lowerBounds (Set.image2 f s t)
• mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds t) : f a b ∈ lowerBounds (Set.image2 f s t)
• mem_lowerBounds_image2_of_mem_upperBounds 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) : f a b ∈ lowerBounds (Set.image2 f s t)
• mem_upperBounds_image2_of_mem_lowerBounds 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ upperBounds (Set.image2 f s t)
• mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a ∈ upperBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ upperBounds (Set.image2 f s t)
• mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds t) : f a b ∈ upperBounds (Set.image2 f s t)
• OrderIso.lowerBounds_image 📋 Mathlib.Order.Bounds.OrderIso
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) {s : Set α} : lowerBounds (⇑f '' s) = ⇑f '' lowerBounds s
• sInf_mem_lowerBounds 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} : sInf s ∈ lowerBounds s
• sInf_le_iff 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} : sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a
• lt_sInf_iff 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {l : α} : l < sInf s ↔ ∃ b, l < b ∧ b ∈ lowerBounds s
• sSup_lowerBounds_eq_sInf 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] (s : Set α) : sSup (lowerBounds s) = sInf s
• GaloisConnection.lowerBounds_u_image 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) (s : Set α) : lowerBounds (u '' s) = l ⁻¹' lowerBounds s
• DirectedOn.csInf_le_iff 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α} (hd : DirectedOn (fun x1 x2 => x2 ≤ x1) s) (h : BddBelow s) (hs : s.Nonempty) : sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a
• csSup_lowerBounds_eq_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (h : BddBelow s) (hs : s.Nonempty) : sSup (lowerBounds s) = sInf s
• csSup_lowerBounds_range 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [Nonempty β] {f : β → α} (hf : BddBelow (Set.range f)) : sSup (lowerBounds (Set.range f)) = ⨅ i, f i
• Monotone.le_csInf_image 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice β] [Preorder α] {f : α → β} (h_mono : Monotone f) {s : Set α} (hs : s.Nonempty) {B : α} (hB : B ∈ lowerBounds s) : f B ≤ sInf (f '' s)
• le_csInf_iff_of_wellFoundedLT 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} {b : α} [WellFoundedLT α] (hs : s.Nonempty) : b ≤ sInf s ↔ b ∈ lowerBounds s
• csInf_le_iff 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h : BddBelow s) (hs : s.Nonempty) : sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a
• exists_between_of_forall_le 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s t : Set α} (sne : s.Nonempty) (tne : t.Nonempty) (hst : ∀ x ∈ s, ∀ y ∈ t, x ≤ y) : (upperBounds s ∩ lowerBounds t).Nonempty
• Set.fintypeOfMemBounds 📋 Mathlib.Order.Interval.Finset.Basic
  {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] {s : Set α} [DecidablePred fun x => x ∈ s] (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds s) : Fintype ↑s
• IsLowerSet.lowerBounds_subset 📋 Mathlib.Order.UpperLower.Basic
  {α : Type u_1} [Preorder α] {s : Set α} (hs : IsLowerSet s) : s.Nonempty → lowerBounds s ⊆ s
• InfClosed.insert_lowerBounds 📋 Mathlib.Order.SupClosed
  {α : Type u_3} [SemilatticeInf α] {s : Set α} {a : α} (hs : InfClosed s) (ha : a ∈ lowerBounds s) : InfClosed (insert a s)
• SupClosed.insert_lowerBounds 📋 Mathlib.Order.SupClosed
  {α : Type u_3} [SemilatticeSup α] {s : Set α} {a : α} (h : SupClosed s) (ha : a ∈ lowerBounds s) : SupClosed (insert a s)
• lowerBounds_infClosure 📋 Mathlib.Order.SupClosed
  {α : Type u_3} [SemilatticeInf α] (s : Set α) : lowerBounds (infClosure s) = lowerBounds s
• Filter.sSup_lowerBounds 📋 Mathlib.Order.Filter.Defs
  {α : Type u_1} (s : Set (Filter α)) : sSup (lowerBounds s) = sInf s
• Antitone.lowerBounds_range_comp_tendsto_atTop 📋 Mathlib.Order.Filter.AtTopBot.Tendsto
  {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder β] [Preorder γ] {l : Filter α} [l.NeBot] {f : β → γ} (hf : Antitone f) {g : α → β} (hg : Filter.Tendsto g l Filter.atTop) : lowerBounds (Set.range (f ∘ g)) = lowerBounds (Set.range f)
• Monotone.lowerBounds_range_comp_tendsto_atBot 📋 Mathlib.Order.Filter.AtTopBot.Tendsto
  {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder β] [Preorder γ] {l : Filter α} [l.NeBot] {f : β → γ} (hf : Monotone f) {g : α → β} (hg : Filter.Tendsto g l Filter.atBot) : lowerBounds (Set.range (f ∘ g)) = lowerBounds (Set.range f)
• Order.IsNormal.mem_lowerBounds_upperBounds_of_isSuccLimit 📋 Mathlib.Order.IsNormal
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} (self : Order.IsNormal f) {a : α} (ha : Order.IsSuccLimit a) : f a ∈ lowerBounds (upperBounds (f '' Set.Iio a))
• Order.IsNormal.mk 📋 Mathlib.Order.IsNormal
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} (strictMono : StrictMono f) (mem_lowerBounds_upperBounds_of_isSuccLimit : ∀ {a : α}, Order.IsSuccLimit a → f a ∈ lowerBounds (upperBounds (f '' Set.Iio a))) : Order.IsNormal f
• Order.isNormal_iff' 📋 Mathlib.Order.IsNormal
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (f : α → β) : Order.IsNormal f ↔ StrictMono f ∧ ∀ {a : α}, Order.IsSuccLimit a → f a ∈ lowerBounds (upperBounds (f '' Set.Iio a))
• IsAtomic.of_isChain_bounded 📋 Mathlib.Order.ZornAtoms
  {α : Type u_1} [PartialOrder α] [OrderBot α] (h : ∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ⊥ ∉ c → ∃ x, x ≠ ⊥ ∧ x ∈ lowerBounds c) : IsAtomic α
• lowerBounds_upperClosure 📋 Mathlib.Order.UpperLower.Closure
  {α : Type u_1} [Preorder α] {s : Set α} : lowerBounds ↑(upperClosure s) = lowerBounds s
• lowerBounds_closure 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] (s : Set α) : lowerBounds (closure s) = lowerBounds s
• Preorder.coneOfLowerBound 📋 Mathlib.CategoryTheory.Limits.Preorder
  {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) {x : C} (h : x ∈ lowerBounds (Set.range F.obj)) : CategoryTheory.Limits.Cone F
• Preorder.conePt_mem_lowerBounds 📋 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.Cone F) : c.pt ∈ lowerBounds (Set.range F.obj)
• Preorder.coneOfLowerBound_pt 📋 Mathlib.CategoryTheory.Limits.Preorder
  {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) {x : C} (h : x ∈ lowerBounds (Set.range F.obj)) : (Preorder.coneOfLowerBound F h).pt = x
• Preorder.coneOfLowerBound_π_app 📋 Mathlib.CategoryTheory.Limits.Preorder
  {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) {x : C} (h : x ∈ lowerBounds (Set.range F.obj)) (i : J) : (Preorder.coneOfLowerBound F h).π.app i = CategoryTheory.homOfLE ⋯
• subset_lowerBounds_add 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {M : Type u_3} [Add M] [Preorder M] [AddLeftMono M] [AddRightMono M] (s t : Set M) : lowerBounds s + lowerBounds t ⊆ lowerBounds (s + t)
• subset_lowerBounds_mul 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {M : Type u_3} [Mul M] [Preorder M] [MulLeftMono M] [MulRightMono M] (s t : Set M) : lowerBounds s * lowerBounds t ⊆ lowerBounds (s * t)
• add_mem_lowerBounds_add 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {M : Type u_3} [Add M] [Preorder M] [AddLeftMono M] [AddRightMono M] {s t : Set M} {a b : M} (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : a + b ∈ lowerBounds (s + t)
• mul_mem_lowerBounds_mul 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {M : Type u_3} [Mul M] [Preorder M] [MulLeftMono M] [MulRightMono M] {s t : Set M} {a b : M} (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : a * b ∈ lowerBounds (s * t)
• smul_lowerBounds_subset_lowerBounds_smul_of_nonneg 📋 Mathlib.Algebra.Order.Module.Pointwise
  {α : Type u_1} {β : Type u_2} [SMul α β] [Preorder α] [Preorder β] [Zero α] [PosSMulMono α β] {a : α} {s : Set β} (ha : 0 ≤ a) : a • lowerBounds s ⊆ lowerBounds (a • s)
• lowerBounds_smul_of_pos 📋 Mathlib.Algebra.Order.Module.Pointwise
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [GroupWithZero α] [Zero β] [MulActionWithZero α β] [PosSMulMono α β] [PosSMulReflectLE α β] {s : Set β} {a : α} (ha : 0 < a) : lowerBounds (a • s) = a • lowerBounds s
• smul_lowerBounds_subset_upperBounds_smul 📋 Mathlib.Algebra.Order.Module.Pointwise
  {α : Type u_1} {β : Type u_2} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulMono α β] {s : Set β} {a : α} (ha : a ≤ 0) : a • lowerBounds s ⊆ upperBounds (a • s)
• smul_upperBounds_subset_lowerBounds_smul 📋 Mathlib.Algebra.Order.Module.Pointwise
  {α : Type u_1} {β : Type u_2} [Ring α] [PartialOrder α] [IsOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulMono α β] {s : Set β} {a : α} (ha : a ≤ 0) : a • upperBounds s ⊆ lowerBounds (a • s)
• lowerBounds_smul_of_neg 📋 Mathlib.Algebra.Order.Module.Pointwise
  {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulMono α β] {s : Set β} {a : α} (ha : a < 0) : lowerBounds (a • s) = a • upperBounds s
• upperBounds_smul_of_neg 📋 Mathlib.Algebra.Order.Module.Pointwise
  {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulMono α β] {s : Set β} {a : α} (ha : a < 0) : upperBounds (a • s) = a • lowerBounds s
• Dense.lowerBounds_image 📋 Mathlib.Topology.Order.IsLUB
  {γ : Type u_2} {α : Type u_3} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {f : γ → α} [TopologicalSpace γ] {S : Set γ} (hS : Dense S) (hf : Continuous f) : lowerBounds (f '' S) = lowerBounds (Set.range f)
• isGLB_of_mem_closure 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {s : Set α} {a : α} (hsa : a ∈ lowerBounds s) (hsf : a ∈ closure s) : IsGLB s a
• isGLB_of_mem_nhds 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {s : Set α} {a : α} {f : Filter α} (hsa : a ∈ lowerBounds s) (hsf : s ∈ f) [(f ⊓ nhds a).NeBot] : IsGLB s a
• IsGLB.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 : MonotoneOn f s) (ha : IsGLB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : b ∈ lowerBounds (f '' s)
• 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)
• zero_mem_lowerBounds_smoothingSeminormSeq_range 📋 Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
  {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (x : R) : 0 ∈ lowerBounds (Set.range fun n => μ (x ^ ↑n) ^ (1 / ↑↑n))
• lowerBounds_iUnion 📋 Mathlib.Order.Bounds.Lattice
  {α : Type u_1} [Preorder α] {ι : Sort u_2} {s : ι → Set α} : lowerBounds (⋃ i, s i) = ⋂ i, lowerBounds (s i)
• gc_lowerBounds_upperBounds 📋 Mathlib.Order.Bounds.Lattice
  {α : Type u_1} [Preorder α] : GaloisConnection (⇑OrderDual.toDual ∘ lowerBounds) (upperBounds ∘ ⇑OrderDual.ofDual)
• gc_upperBounds_lowerBounds 📋 Mathlib.Order.Bounds.Lattice
  {α : Type u_1} [Preorder α] : GaloisConnection (⇑OrderDual.toDual ∘ upperBounds) (lowerBounds ∘ ⇑OrderDual.ofDual)
• lowerPolar_le 📋 Mathlib.Order.Concept
  {β : Type u_3} {t : Set β} [LE β] : lowerPolar (fun x1 x2 => x1 ≤ x2) t = lowerBounds t
• DedekindCut.lowerBounds_right 📋 Mathlib.Order.Completion
  {α : Type u_1} [Preorder α] (A : DedekindCut α) : lowerBounds A.right = A.left
• DedekindCut.image_left_subset_lowerBounds 📋 Mathlib.Order.Completion
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) (A : DedekindCut α) : f '' A.left ⊆ lowerBounds (f '' A.right)
• lowerBounds_countableInfClosure 📋 Mathlib.Order.CountableSupClosed
  {α : Type u_2} [Preorder α] (s : Set α) : lowerBounds (countableInfClosure s) = lowerBounds s

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