Loogle!

Result

Found 134 declarations mentioning upperBounds.

• upperBounds 📋 Mathlib.Order.Bounds.Defs
  {α : Type u_1} [LE α] (s : Set α) : Set α
• upperBounds_empty 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] : upperBounds ∅ = Set.univ
• Set.Nonempty.bddBelow_upperBounds 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} (hs : s.Nonempty) : BddBelow (upperBounds s)
• upperBounds_Iic 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a : α} : upperBounds (Set.Iic a) = Set.Ici 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)
• upperBounds_singleton 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a : α} : upperBounds {a} = Set.Ici a
• NoTopOrder.upperBounds_univ 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] [NoTopOrder α] : upperBounds Set.univ = ∅
• mem_upperBounds_univ 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a : α} : a ∈ upperBounds Set.univ ↔ IsTop a
• isGLB_upperBounds 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsGLB (upperBounds s) a ↔ IsLUB s a
• IsGreatest.upperBounds_eq 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsGreatest s a) : upperBounds s = Set.Ici a
• IsLUB.upperBounds_eq 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} (h : IsLUB s a) : upperBounds s = Set.Ici a
• upperBounds_Icc 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a b : α} (h : a ≤ b) : upperBounds (Set.Icc a b) = Set.Ici b
• upperBounds_Ioc 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a b : α} (h : a < b) : upperBounds (Set.Ioc a b) = Set.Ici b
• mem_upperBounds_iff_subset_Iic 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} : a ∈ upperBounds s ↔ s ⊆ Set.Iic a
• top_mem_upperBounds 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] [OrderTop α] (s : Set α) : ⊤ ∈ upperBounds s
• upperBounds_mono_of_isCofinalFor 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s t : Set α} (hst : IsCofinalFor s t) : upperBounds t ⊆ upperBounds s
• upperBounds_mono_set 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] ⦃s t : Set α⦄ (hst : s ⊆ t) : upperBounds t ⊆ upperBounds s
• 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_iff_le_iff 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} : IsLUB s a ↔ ∀ (b : α), a ≤ b ↔ b ∈ upperBounds s
• mem_upperBounds 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} {a : α} : a ∈ upperBounds s ↔ ∀ x ∈ s, x ≤ a
• upperBounds_insert 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] (a : α) (s : Set α) : upperBounds (insert a s) = Set.Ici a ∩ upperBounds s
• 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
• OrderTop.upperBounds_univ 📋 Mathlib.Order.Bounds.Basic
  {γ : Type u_3} [PartialOrder γ] [OrderTop γ] : upperBounds Set.univ = {⊤}
• upperBounds_union 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s t : Set α} : upperBounds (s ∪ t) = upperBounds s ∩ upperBounds t
• upperBounds_mono_mem 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s : Set α} ⦃a b : α⦄ (hab : a ≤ b) : a ∈ upperBounds s → b ∈ upperBounds s
• union_upperBounds_subset_upperBounds_inter 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {s t : Set α} : upperBounds s ∪ upperBounds t ⊆ upperBounds (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
• 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
• upperBounds_mono 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] ⦃s t : Set α⦄ (hst : s ⊆ t) ⦃a b : α⦄ (hab : a ≤ b) : a ∈ upperBounds t → b ∈ upperBounds 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
• upperBounds_Ico 📋 Mathlib.Order.Bounds.Basic
  {γ : Type u_3} [SemilatticeInf γ] [DenselyOrdered γ] {a b : γ} (hab : b < a) : upperBounds (Set.Ico b a) = Set.Ici a
• upperBounds_Ioo 📋 Mathlib.Order.Bounds.Basic
  {γ : Type u_3} [SemilatticeInf γ] [DenselyOrdered γ] {a b : γ} (hab : b < a) : upperBounds (Set.Ioo b a) = Set.Ici a
• isGreatest_union_iff 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {a : α} {s t : Set α} : IsGreatest (s ∪ t) a ↔ IsGreatest s a ∧ a ∈ upperBounds t ∨ a ∈ upperBounds s ∧ IsGreatest t a
• upperBounds_Iio 📋 Mathlib.Order.Bounds.Basic
  {γ : Type u_3} [LinearOrder γ] [DenselyOrdered γ] {a : γ} : upperBounds (Set.Iio a) = Set.Ici a
• upperBounds_prod 📋 Mathlib.Order.Bounds.Basic
  {α : 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
• 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_upperBounds_subset_upperBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {s : Set α} : f '' upperBounds s ⊆ upperBounds (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_upperBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {a : α} {s : Set α} (Ha : a ∈ upperBounds s) : f a ∈ upperBounds (f '' s)
• AntitoneOn.map_bddAbove 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) : (upperBounds s ∩ t).Nonempty → BddBelow (f '' s)
• MonotoneOn.map_bddAbove 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) : (upperBounds s ∩ t).Nonempty → BddAbove (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_upperBounds_subset_upperBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) : f '' (upperBounds s ∩ t) ⊆ upperBounds (f '' s)
• MonotoneOn.mem_upperBounds_image_self 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : MonotoneOn f t) : a ∈ upperBounds t → a ∈ t → f a ∈ upperBounds (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_upperBounds_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 ∈ upperBounds s) (Hat : a ∈ t) : f a ∈ upperBounds (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_upperBounds_image 📋 Mathlib.Order.Bounds.Image
  {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {a : α} {s : Set α} (hf : StrictMono f) : f a ∈ upperBounds (f '' s) ↔ a ∈ upperBounds s
• 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 📋 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 (upperBounds s) (upperBounds 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_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 📋 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 ∈ upperBounds s) (hb : b ∈ upperBounds t) : f a b ∈ upperBounds (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)
• Monotone.upperBounds_image_of_directedOn_prod 📋 Mathlib.Order.Bounds.Image
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {γ : Type u_3} [Preorder γ] {g : α × β → γ} (hg : Monotone g) {d : Set (α × β)} (hd : DirectedOn (fun x1 x2 => x1 ≤ x2) d) : upperBounds (g '' d) = upperBounds (g '' (Prod.fst '' d) ×ˢ (Prod.snd '' d))
• OrderIso.upperBounds_image 📋 Mathlib.Order.Bounds.OrderIso
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) {s : Set α} : upperBounds (⇑f '' s) = ⇑f '' upperBounds s
• sSup_mem_upperBounds 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} : sSup s ∈ upperBounds s
• le_sSup_iff 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} : a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b
• sSup_lt_iff 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {l : α} : sSup s < l ↔ ∃ b < l, b ∈ upperBounds s
• sInf_upperBounds_eq_sSup 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] (s : Set α) : sInf (upperBounds s) = sSup s
• GaloisConnection.upperBounds_l_image 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (s : Set α) : upperBounds (l '' s) = u ⁻¹' upperBounds s
• DirectedOn.le_csSup_iff 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_1} [ConditionallyCompletePartialOrderSup α] {s : Set α} {a : α} (hd : DirectedOn (fun x1 x2 => x1 ≤ x2) s) (h : BddAbove s) (hs : s.Nonempty) : a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b
• csInf_upperBounds_eq_csSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (h : BddAbove s) (hs : s.Nonempty) : sInf (upperBounds s) = sSup s
• csSup_le' 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : a ∈ upperBounds s) : sSup s ≤ a
• csInf_upperBounds_range 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [Nonempty β] {f : β → α} (hf : BddAbove (Set.range f)) : sInf (upperBounds (Set.range f)) = ⨆ i, f i
• Monotone.csSup_image_le 📋 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 ∈ upperBounds s) : sSup (f '' s) ≤ f B
• csSup_le_iff_of_wellFoundedGT 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} {b : α} [WellFoundedGT α] (hs : s.Nonempty) : sSup s ≤ b ↔ b ∈ upperBounds s
• 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
• le_csSup_iff 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h : BddAbove s) (hs : s.Nonempty) : a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b
• le_csSup_iff' 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : BddAbove s) : a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b
• 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
• IsUpperSet.upperBounds_subset 📋 Mathlib.Order.UpperLower.Basic
  {α : Type u_1} [Preorder α] {s : Set α} (hs : IsUpperSet s) : s.Nonempty → upperBounds s ⊆ s
• InfClosed.insert_upperBounds 📋 Mathlib.Order.SupClosed
  {α : Type u_3} [SemilatticeInf α] {s : Set α} {a : α} (h : InfClosed s) (ha : a ∈ upperBounds s) : InfClosed (insert a s)
• SupClosed.insert_upperBounds 📋 Mathlib.Order.SupClosed
  {α : Type u_3} [SemilatticeSup α] {s : Set α} {a : α} (hs : SupClosed s) (ha : a ∈ upperBounds s) : SupClosed (insert a s)
• upperBounds_supClosure 📋 Mathlib.Order.SupClosed
  {α : Type u_3} [SemilatticeSup α] (s : Set α) : upperBounds (supClosure s) = upperBounds s
• upperBounds_range_partialSups 📋 Mathlib.Order.PartialSups
  {α : Type u_1} {ι : Type u_3} [SemilatticeSup α] [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → α) : upperBounds (Set.range ⇑(partialSups f)) = upperBounds (Set.range f)
• Antitone.upperBounds_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 : Antitone f) {g : α → β} (hg : Filter.Tendsto g l Filter.atBot) : upperBounds (Set.range (f ∘ g)) = upperBounds (Set.range f)
• Monotone.upperBounds_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 : Monotone f) {g : α → β} (hg : Filter.Tendsto g l Filter.atTop) : upperBounds (Set.range (f ∘ g)) = upperBounds (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))
• IsCoatomic.of_isChain_bounded 📋 Mathlib.Order.ZornAtoms
  {α : Type u_1} [PartialOrder α] [OrderTop α] (h : ∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c) : IsCoatomic α
• upperBounds_lowerClosure 📋 Mathlib.Order.UpperLower.Closure
  {α : Type u_1} [Preorder α] {s : Set α} : upperBounds ↑(lowerClosure s) = upperBounds s
• upperBounds_closure 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] (s : Set α) : upperBounds (closure s) = upperBounds s
• Preorder.coconeOfUpperBound 📋 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 ∈ upperBounds (Set.range F.obj)) : CategoryTheory.Limits.Cocone F
• Preorder.coconePt_mem_upperBounds 📋 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) : c.pt ∈ upperBounds (Set.range F.obj)
• Preorder.coconeOfUpperBound_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 ∈ upperBounds (Set.range F.obj)) : (Preorder.coconeOfUpperBound F h).pt = x
• Preorder.coconeOfUpperBound_ι_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 ∈ upperBounds (Set.range F.obj)) (i : J) : (Preorder.coconeOfUpperBound F h).ι.app i = CategoryTheory.homOfLE ⋯
• subset_upperBounds_add 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {M : Type u_3} [Add M] [Preorder M] [AddLeftMono M] [AddRightMono M] (s t : Set M) : upperBounds s + upperBounds t ⊆ upperBounds (s + t)
• subset_upperBounds_mul 📋 Mathlib.Algebra.Order.Group.Pointwise.Bounds
  {M : Type u_3} [Mul M] [Preorder M] [MulLeftMono M] [MulRightMono M] (s t : Set M) : upperBounds s * upperBounds t ⊆ upperBounds (s * t)
• add_mem_upperBounds_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 ∈ upperBounds s) (hb : b ∈ upperBounds t) : a + b ∈ upperBounds (s + t)
• mul_mem_upperBounds_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 ∈ upperBounds s) (hb : b ∈ upperBounds t) : a * b ∈ upperBounds (s * t)
• ENNReal.coe_mem_upperBounds 📋 Mathlib.Basic.ENNReal.Basic
  {r : NNReal} {s : Set NNReal} : ↑r ∈ upperBounds (ENNReal.ofNNReal '' s) ↔ r ∈ upperBounds s
• smul_upperBounds_subset_upperBounds_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 • upperBounds s ⊆ upperBounds (a • s)
• upperBounds_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) : upperBounds (a • s) = a • upperBounds 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.upperBounds_image 📋 Mathlib.Topology.Order.IsLUB
  {γ : Type u_2} {α : Type u_3} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {f : γ → α} [TopologicalSpace γ] {S : Set γ} (hS : Dense S) (hf : Continuous f) : upperBounds (f '' S) = upperBounds (Set.range f)
• 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.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 : AntitoneOn f s) (ha : IsGLB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) : b ∈ upperBounds (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)
• FirstOrder.Language.DirectLimit.unify 📋 Mathlib.ModelTheory.DirectLimit
  {L : FirstOrder.Language} {ι : Type v} [Preorder ι] {G : ι → Type w} [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) {α : Type u_1} (x : α → FirstOrder.Language.Structure.Sigma f) (i : ι) (h : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) (a : α) : G i
• FirstOrder.Language.DirectLimit.relMap_equiv_unify 📋 Mathlib.ModelTheory.DirectLimit
  {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [IsDirectedOrder ι] [DirectedSystem G fun i j h => ⇑(f i j h)] [Nonempty ι] {n : ℕ} (R : L.Relations n) (x : Fin n → FirstOrder.Language.Structure.Sigma f) (i : ι) (hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) : FirstOrder.Language.Structure.RelMap R x = FirstOrder.Language.Structure.RelMap R (FirstOrder.Language.DirectLimit.unify f x i hi)
• FirstOrder.Language.DirectLimit.relMap_unify_equiv 📋 Mathlib.ModelTheory.DirectLimit
  {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [IsDirectedOrder ι] [DirectedSystem G fun i j h => ⇑(f i j h)] {n : ℕ} (R : L.Relations n) (x : Fin n → FirstOrder.Language.Structure.Sigma f) (i j : ι) (hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) (hj : j ∈ upperBounds (Set.range (Sigma.fst ∘ x))) : FirstOrder.Language.Structure.RelMap R (FirstOrder.Language.DirectLimit.unify f x i hi) = FirstOrder.Language.Structure.RelMap R (FirstOrder.Language.DirectLimit.unify f x j hj)
• FirstOrder.Language.DirectLimit.funMap_equiv_unify 📋 Mathlib.ModelTheory.DirectLimit
  {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [IsDirectedOrder ι] [DirectedSystem G fun i j h => ⇑(f i j h)] [Nonempty ι] {n : ℕ} (F : L.Functions n) (x : Fin n → FirstOrder.Language.Structure.Sigma f) (i : ι) (hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) : FirstOrder.Language.Structure.funMap F x ≈ FirstOrder.Language.Structure.Sigma.mk f i (FirstOrder.Language.Structure.funMap F (FirstOrder.Language.DirectLimit.unify f x i hi))
• FirstOrder.Language.DirectLimit.funMap_unify_equiv 📋 Mathlib.ModelTheory.DirectLimit
  {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [IsDirectedOrder ι] [DirectedSystem G fun i j h => ⇑(f i j h)] {n : ℕ} (F : L.Functions n) (x : Fin n → FirstOrder.Language.Structure.Sigma f) (i j : ι) (hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) (hj : j ∈ upperBounds (Set.range (Sigma.fst ∘ x))) : FirstOrder.Language.Structure.Sigma.mk f i (FirstOrder.Language.Structure.funMap F (FirstOrder.Language.DirectLimit.unify f x i hi)) ≈ FirstOrder.Language.Structure.Sigma.mk f j (FirstOrder.Language.Structure.funMap F (FirstOrder.Language.DirectLimit.unify f x j hj))
• FirstOrder.Language.DirectLimit.exists_unify_eq 📋 Mathlib.ModelTheory.DirectLimit
  {L : FirstOrder.Language} {ι : Type v} [Preorder ι] (G : ι → Type w) [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [IsDirectedOrder ι] [DirectedSystem G fun i j h => ⇑(f i j h)] [Nonempty ι] {α : Type u_1} [Finite α] {x y : α → FirstOrder.Language.Structure.Sigma f} (xy : x ≈ y) : ∃ i, ∃ (hx : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) (hy : i ∈ upperBounds (Set.range (Sigma.fst ∘ y))), FirstOrder.Language.DirectLimit.unify f x i hx = FirstOrder.Language.DirectLimit.unify f y i hy
• FirstOrder.Language.DirectLimit.comp_unify 📋 Mathlib.ModelTheory.DirectLimit
  {L : FirstOrder.Language} {ι : Type v} [Preorder ι] {G : ι → Type w} [(i : ι) → L.Structure (G i)] (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [DirectedSystem G fun i j h => ⇑(f i j h)] {α : Type u_1} {x : α → FirstOrder.Language.Structure.Sigma f} {i j : ι} (ij : i ≤ j) (h : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) : ⇑(f i j ij) ∘ FirstOrder.Language.DirectLimit.unify f x i h = FirstOrder.Language.DirectLimit.unify f x j ⋯
• upperBounds_iUnion 📋 Mathlib.Order.Bounds.Lattice
  {α : Type u_1} [Preorder α] {ι : Sort u_2} {s : ι → Set α} : upperBounds (⋃ i, s i) = ⋂ i, upperBounds (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)
• upperPolar_le 📋 Mathlib.Order.Concept
  {α : Type u_2} {s : Set α} [LE α] : upperPolar (fun x1 x2 => x1 ≤ x2) s = upperBounds s
• DedekindCut.upperBounds_left 📋 Mathlib.Order.Completion
  {α : Type u_1} [Preorder α] (A : DedekindCut α) : upperBounds A.left = A.right
• DedekindCut.image_right_subset_upperBounds 📋 Mathlib.Order.Completion
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) (A : DedekindCut α) : f '' A.right ⊆ upperBounds (f '' A.left)
• upperBounds_countableSupClosure 📋 Mathlib.Order.CountableSupClosed
  {α : Type u_2} [Preorder α] (s : Set α) : upperBounds (countableSupClosure s) = upperBounds 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 69fae59