Loogle!

Result

Found 3777 declarations mentioning Bot.bot. Of these, only the first 200 are shown.

• Bot.bot 📋 Mathlib.Order.Notation
  {α : Type u_1} [self : Bot α] : α
• Bot.ext 📋 Mathlib.Order.Notation
  {α : Type u_1} {x y : Bot α} (bot : ⊥ = ⊥) : x = y
• Bot.ext_iff 📋 Mathlib.Order.Notation
  {α : Type u_1} {x y : Bot α} : x = y ↔ ⊥ = ⊥
• Equiv.bot_def 📋 Mathlib.Order.OrderDual
  {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Bot β] : ⊥ = e.symm ⊥
• bot_eq_false 📋 Mathlib.Order.BoundedOrder.Basic
  : ⊥ = false
• isBot_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [LE α] [OrderBot α] : IsBot ⊥
• OrderBot.mk 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [LE α] [toBot : Bot α] (bot_le : ∀ (a : α), ⊥ ≤ a) : OrderBot α
• ULift.down_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Bot α] : ⊥.down = ⊥
• bot_le 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [LE α] [OrderBot α] {a : α} : ⊥ ≤ a
• OrderBot.bot_le 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} {inst✝ : LE α} [self : OrderBot α] (a : α) : ⊥ ≤ a
• ULift.up_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Bot α] : { down := ⊥ } = ⊥
• isMin_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Preorder α] [OrderBot α] : IsMin ⊥
• Prod.fst_bot 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) (β : Type v) [Bot α] [Bot β] : ⊥.1 = ⊥
• Prod.snd_bot 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) (β : Type v) [Bot α] [Bot β] : ⊥.2 = ⊥
• not_covBy_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Preorder α] [OrderBot α] {a : α} : ¬a ⋖ ⊥
• not_lt_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Preorder α] [OrderBot α] {a : α} : ¬a < ⊥
• Pi.bot_apply 📋 Mathlib.Order.BoundedOrder.Basic
  {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → Bot (α' i)] (i : ι) : ⊥ i = ⊥
• Pi.bot_def 📋 Mathlib.Order.BoundedOrder.Basic
  {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → Bot (α' i)] : ⊥ = fun x => ⊥
• Subtype.orderBot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} {p : α → Prop} [LE α] [OrderBot α] (hbot : p ⊥) : OrderBot { x // p x }
• ne_bot_of_gt 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Preorder α] [OrderBot α] {a b : α} (h : b < a) : a ≠ ⊥
• LT.lt.ne_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Preorder α] [OrderBot α] {a b : α} (h : b < a) : a ≠ ⊥
• not_isMax_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] [Nontrivial α] : ¬IsMax ⊥
• bot_lt_of_lt 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Preorder α] [OrderBot α] {a b : α} (h : b < a) : ⊥ < a
• not_isMin_iff_bot_lt 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Preorder α] [OrderBot α] {a : α} : ¬IsMin a ↔ ⊥ < a
• IsBot.rec 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [LE α] {motive : (x : α) → IsBot x → Sort u_1} (bot : [inst : OrderBot α] → motive ⊥ ⋯) (x : α) (hx : IsBot x) : motive x hx
• LT.lt.bot_lt 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Preorder α] [OrderBot α] {a b : α} (h : b < a) : ⊥ < a
• IsBot.eq_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] {a : α} : IsBot a → a = ⊥
• IsMin.eq_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] {a : α} : IsMin a → a = ⊥
• isBot_iff_eq_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] {a : α} : IsBot a ↔ a = ⊥
• isMin_iff_eq_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] {a : α} : IsMin a ↔ a = ⊥
• Pi.bot_comp 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Bot γ] (x : α → β) : ⊥ ∘ x = ⊥
• ite_ne_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Bot α] {p : Prop} [Decidable p] {a b : α} (ha : p → a ≠ ⊥) (hb : ¬p → b ≠ ⊥) : (if p then a else b) ≠ ⊥
• not_isBot_iff_ne_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] {a : α} : ¬IsBot a ↔ a ≠ ⊥
• not_isMin_iff_ne_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] {a : α} : ¬IsMin a ↔ a ≠ ⊥
• Subtype.boundedOrder 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} {p : α → Prop} [LE α] [BoundedOrder α] (hbot : p ⊥) (htop : p ⊤) : BoundedOrder (Subtype p)
• OrderDual.ofDual_bot 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) [Top α] : OrderDual.ofDual ⊥ = ⊤
• OrderDual.ofDual_top 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) [Bot α] : OrderDual.ofDual ⊤ = ⊥
• OrderDual.toDual_bot 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) [Bot α] : OrderDual.toDual ⊥ = ⊤
• OrderDual.toDual_top 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) [Top α] : OrderDual.toDual ⊤ = ⊥
• bot_lt_iff_not_le_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Preorder α] [OrderBot α] {a : α} : ⊥ < a ↔ ¬a ≤ ⊥
• bot_unique 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : a ≤ ⊥) : a = ⊥
• Ne.bot_lt 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : a ≠ ⊥) : ⊥ < a
• Ne.bot_lt' 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : ⊥ ≠ a) : ⊥ < a
• OrderBot.lift 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} {β : Type v} [LE α] [Bot α] [LE β] [OrderBot β] (f : α → β) (map_le : ∀ (b a : α), f b ≤ f a → b ≤ a) (map_bot : f ⊥ = ⊥) : OrderBot α
• bot_lt_iff_ne_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] {a : α} : ⊥ < a ↔ a ≠ ⊥
• eq_bot_iff 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] {a : α} : a = ⊥ ↔ a ≤ ⊥
• eq_bot_or_bot_lt 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] (a : α) : a = ⊥ ∨ ⊥ < a
• le_bot_iff 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] {a : α} : a ≤ ⊥ ↔ a = ⊥
• dite_ne_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Bot α] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} (ha : ∀ (h : p), a h ≠ ⊥) (hb : ∀ (h : ¬p), b h ≠ ⊥) : (if h : p then a h else b h) ≠ ⊥
• not_bot_lt_iff 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] {a : α} : ¬⊥ < a ↔ a = ⊥
• OrderDual.toDual_eq_bot 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) [Top α] {a : α} : OrderDual.toDual a = ⊥ ↔ a = ⊤
• OrderDual.toDual_eq_top 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) [Bot α] {a : α} : OrderDual.toDual a = ⊤ ↔ a = ⊥
• OrderDual.ofDual_eq_bot 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) [Bot α] {a : αᵒᵈ} : OrderDual.ofDual a = ⊥ ↔ a = ⊤
• OrderDual.ofDual_eq_top 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) [Top α] {a : αᵒᵈ} : OrderDual.ofDual a = ⊤ ↔ a = ⊥
• eq_bot_mono 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] {a b : α} (h : b ≤ a) (h₂ : a = ⊥) : b = ⊥
• ne_bot_of_le_ne_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] {a b : α} (hb : b ≠ ⊥) (hab : b ≤ a) : a ≠ ⊥
• bot_ne_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [BoundedOrder α] [Nontrivial α] : ⊥ ≠ ⊤
• subsingleton_of_bot_eq_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [BoundedOrder α] (hα : ⊥ = ⊤) : Subsingleton α
• subsingleton_of_top_eq_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [BoundedOrder α] (hα : ⊤ = ⊥) : Subsingleton α
• top_ne_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [BoundedOrder α] [Nontrivial α] : ⊤ ≠ ⊥
• subsingleton_iff_bot_eq_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [BoundedOrder α] : ⊥ = ⊤ ↔ Subsingleton α
• subsingleton_iff_top_eq_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [BoundedOrder α] : ⊤ = ⊥ ↔ Subsingleton α
• bot_lt_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [BoundedOrder α] [Nontrivial α] : ⊥ < ⊤
• subsingleton_of_top_le_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [BoundedOrder α] (h : ⊤ ≤ ⊥) : Subsingleton α
• bot_notMem_iff 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderBot α] {s : Set α} : ⊥ ∉ s ↔ ∀ x ∈ s, ⊥ < x
• BoundedOrder.lift 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} {β : Type v} [LE α] [Top α] [Bot α] [LE β] [BoundedOrder β] (f : α → β) (map_le : ∀ (a b : α), f a ≤ f b → a ≤ b) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) : BoundedOrder α
• OrderBot.ext_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u_1} {hA : PartialOrder α} (A : OrderBot α) {hB : PartialOrder α} (B : OrderBot α) (H : ∀ (y x : α), y ≤ x ↔ y ≤ x) : ⊥ = ⊥
• eq_bot_of_bot_eq_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [BoundedOrder α] (hα : ⊥ = ⊤) (x : α) : x = ⊥
• eq_bot_of_top_eq_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [BoundedOrder α] (hα : ⊤ = ⊥) (x : α) : x = ⊥
• eq_top_of_bot_eq_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [BoundedOrder α] (hα : ⊥ = ⊤) (x : α) : x = ⊤
• eq_top_of_top_eq_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [BoundedOrder α] (hα : ⊤ = ⊥) (x : α) : x = ⊤
• Subtype.coe_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} {p : α → Prop} [PartialOrder α] [OrderBot α] [OrderBot (Subtype p)] (hbot : p ⊥) : ↑⊥ = ⊥
• Subtype.mk_bot 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} {p : α → Prop} [PartialOrder α] [OrderBot α] [OrderBot (Subtype p)] (hbot : p ⊥) : ⟨⊥, hbot⟩ = ⊥
• Subtype.mk_eq_bot_iff 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} {p : α → Prop} [PartialOrder α] [OrderBot α] [OrderBot (Subtype p)] (hbot : p ⊥) {x : α} (hx : p x) : ⟨x, hx⟩ = ⊥ ↔ x = ⊥
• Subtype.coe_eq_bot_iff 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} {p : α → Prop} [PartialOrder α] [OrderBot α] [OrderBot (Subtype p)] (hbot : p ⊥) {x : { x // p x }} : ↑x = ⊥ ↔ x = ⊥
• bot_sup_eq 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u_1} [SemilatticeSup α] [OrderBot α] (a : α) : ⊥ ⊔ a = a
• sup_bot_eq 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u_1} [SemilatticeSup α] [OrderBot α] (a : α) : a ⊔ ⊥ = a
• bot_inf_eq 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u_1} [SemilatticeInf α] [OrderBot α] (a : α) : ⊥ ⊓ a = ⊥
• inf_bot_eq 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u_1} [SemilatticeInf α] [OrderBot α] (a : α) : a ⊓ ⊥ = ⊥
• max_bot_left 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u_1} [LinearOrder α] [OrderBot α] (a : α) : max ⊥ a = a
• max_bot_right 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u_1} [LinearOrder α] [OrderBot α] (a : α) : max a ⊥ = a
• WellFoundedLT.induction_bot 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u_1} [Preorder α] [WellFoundedLT α] [OrderBot α] {P : α → Prop} (hexists : ∃ M, P M) (hind : ∀ (N : α), N ≠ ⊥ → P N → ∃ M, N > M ∧ P M) : P ⊥
• sup_eq_bot_iff 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u_1} [SemilatticeSup α] [OrderBot α] {a b : α} : a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥
• min_bot_left 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u_1} [LinearOrder α] [OrderBot α] (a : α) : min ⊥ a = ⊥
• min_bot_right 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u_1} [LinearOrder α] [OrderBot α] (a : α) : min a ⊥ = ⊥
• min_ne_bot 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u_1} [LinearOrder α] [OrderBot α] {a b : α} (ha : a ≠ ⊥) (hb : b ≠ ⊥) : min a b ≠ ⊥
• max_eq_bot 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u_1} [LinearOrder α] [OrderBot α] {a b : α} : max a b = ⊥ ↔ a = ⊥ ∧ b = ⊥
• min_eq_bot 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u_1} [LinearOrder α] [OrderBot α] {a b : α} : min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥
• disjoint_bot_left 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} : Disjoint ⊥ a
• disjoint_bot_right 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} : Disjoint a ⊥
• Disjoint.eq_bot_of_self 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} : Disjoint a a → a = ⊥
• disjoint_self 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} : Disjoint a a ↔ a = ⊥
• Disjoint.ne 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} (ha : a ≠ ⊥) (hab : Disjoint a b) : a ≠ b
• Disjoint.eq_bot_of_ge 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} (hab : Disjoint a b) : b ≤ a → b = ⊥
• Disjoint.eq_bot_of_le 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} (hab : Disjoint a b) (h : a ≤ b) : a = ⊥
• disjoint_of_le_iff_left_eq_bot 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} (h : a ≤ b) : Disjoint a b ↔ a = ⊥
• isComplemented_bot 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [Lattice α] [BoundedOrder α] : IsComplemented ⊥
• Disjoint.eq_bot 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} : Disjoint a b → a ⊓ b = ⊥
• disjoint_iff 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} : Disjoint a b ↔ a ⊓ b = ⊥
• Disjoint.eq_iff 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} (hab : Disjoint a b) : a = b ↔ a = ⊥ ∧ b = ⊥
• Disjoint.le_bot 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} : Disjoint a b → a ⊓ b ≤ ⊥
• Disjoint.ne_iff 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} (hab : Disjoint a b) : a ≠ b ↔ a ≠ ⊥ ∨ b ≠ ⊥
• Disjoint.out 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} (h : Disjoint a b) (x : α) : x ≤ a → x ≤ b → x = ⊥
• disjoint_iff_inf_le 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} : Disjoint a b ↔ a ⊓ b ≤ ⊥
• Disjoint.right_lt_sup_of_left_ne_bot 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [SemilatticeSup α] [OrderBot α] {a b : α} (h : Disjoint a b) (ha : a ≠ ⊥) : b < a ⊔ b
• bot_codisjoint 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a : α} : Codisjoint ⊥ a ↔ a = ⊤
• codisjoint_bot 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a : α} : Codisjoint a ⊥ ↔ a = ⊤
• disjoint_top 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a : α} : Disjoint a ⊤ ↔ a = ⊥
• top_disjoint 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a : α} : Disjoint ⊤ a ↔ a = ⊥
• IsCompl.inf_eq_bot 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [Lattice α] [BoundedOrder α] {x y : α} (h : IsCompl x y) : x ⊓ y = ⊥
• Codisjoint.ne_bot_of_ne_top 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a b : α} (h : Codisjoint a b) (ha : a ≠ ⊤) : b ≠ ⊥
• Disjoint.ne_top_of_ne_bot 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a b : α} (h : Disjoint a b) (ha : a ≠ ⊥) : b ≠ ⊤
• isCompl_bot_top 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [Lattice α] [BoundedOrder α] : IsCompl ⊥ ⊤
• isCompl_top_bot 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [Lattice α] [BoundedOrder α] : IsCompl ⊤ ⊥
• eq_bot_of_isCompl_top 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [Lattice α] [BoundedOrder α] {x : α} (h : IsCompl x ⊤) : x = ⊥
• eq_bot_of_top_isCompl 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [Lattice α] [BoundedOrder α] {x : α} (h : IsCompl ⊤ x) : x = ⊥
• eq_top_of_bot_isCompl 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [Lattice α] [BoundedOrder α] {x : α} (h : IsCompl ⊥ x) : x = ⊤
• eq_top_of_isCompl_bot 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [Lattice α] [BoundedOrder α] {x : α} (h : IsCompl x ⊥) : x = ⊤
• disjoint_subtype_iff 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [SemilatticeInf α] [OrderBot α] {pr : α → Prop} (Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)) (hbot : pr ⊥) {a b : Subtype pr} : Disjoint a b ↔ Disjoint ↑a ↑b
• IsCompl.inf_left_eq_bot_iff 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x y z : α} (h : IsCompl y z) : x ⊓ y = ⊥ ↔ x ≤ z
• IsCompl.inf_right_eq_bot_iff 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x y z : α} (h : IsCompl y z) : x ⊓ z = ⊥ ↔ x ≤ y
• IsCompl.of_eq 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [Lattice α] [BoundedOrder α] {x y : α} (h₁ : x ⊓ y = ⊥) (h₂ : x ⊔ y = ⊤) : IsCompl x y
• Complementeds.coe_bot 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [Lattice α] [BoundedOrder α] : ↑⊥ = ⊥
• IsCompl.of_le 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [Lattice α] [BoundedOrder α] {x y : α} (h₁ : x ⊓ y ≤ ⊥) (h₂ : ⊤ ≤ x ⊔ y) : IsCompl x y
• Complementeds.mk_bot 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [Lattice α] [BoundedOrder α] : ⟨⊥, ⋯⟩ = ⊥
• Prop.bot_eq_false 📋 Mathlib.Order.PropInstances
  : ⊥ = False
• Prop.decidablePredBot 📋 Mathlib.Order.PropInstances
  {α : Type u} : DecidablePred ⊥
• Pi.instSymmBotForallForallProp 📋 Mathlib.Order.PropInstances
  (α : Type u_4) : Std.Symm ⊥
• Prop.decidableRelBot 📋 Mathlib.Order.PropInstances
  {α : Type u} : DecidableRel ⊥
• Pi.eq_bot_iff_irrefl_of_subsingleton 📋 Mathlib.Order.PropInstances
  {α : Type u_2} [Subsingleton α] {r : α → α → Prop} : r = ⊥ ↔ Std.Irrefl r
• Set.ofPred_bot 📋 Mathlib.Data.Set.Basic
  {α : Type u} : {_x | ⊥} = ∅
• Set.setOf_bot 📋 Mathlib.Data.Set.Basic
  {α : Type u} : {_x | ⊥} = ∅
• Set.bot_eq_empty 📋 Mathlib.Data.Set.Basic
  {α : Type u} : ⊥ = ∅
• GaloisConnection.l_u_bot 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] [OrderBot α] {u : α → β} {l : β → α} (gc : GaloisConnection l u) : l (u ⊥) = ⊥
• GaloisCoinsertion.u_bot 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} {u : α → β} {l : β → α} [Preorder α] [PartialOrder β] [OrderBot α] [OrderBot β] (gi : GaloisCoinsertion l u) : u ⊥ = ⊥
• GaloisConnection.l_bot 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] [OrderBot α] [OrderBot β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) : l ⊥ = ⊥
• GaloisConnection.l_eq_bot 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] [OrderBot α] {u : α → β} {l : β → α} (gc : GaloisConnection l u) {x : β} : l x = ⊥ ↔ x ≤ u ⊥
• PUnit.bot_eq 📋 Mathlib.Order.Heyting.Basic
  : ⊥ = PUnit.unit
• sdiff_bot 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} : a \ ⊥ = a
• sdiff_self 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} : a \ a = ⊥
• sdiff_sdiff_self 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b : α} : (a \ b) \ a = ⊥
• himp_bot 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] (a : α) : a ⇨ ⊥ = aᶜ
• HeytingAlgebra.himp_bot 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_4} [self : HeytingAlgebra α] (a : α) : a ⇨ ⊥ = aᶜ
• compl_inf_eq_bot 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] {a : α} : aᶜ ⊓ a = ⊥
• compl_inf_self 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] (a : α) : aᶜ ⊓ a = ⊥
• inf_compl_eq_bot 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] {a : α} : a ⊓ aᶜ = ⊥
• inf_compl_self 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] (a : α) : a ⊓ aᶜ = ⊥
• bot_sdiff 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} : ⊥ \ a = ⊥
• sdiff_eq_bot_iff 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b : α} : b \ a = ⊥ ↔ b ≤ a
• HeytingAlgebra.mk 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_4} [toGeneralizedHeytingAlgebra : GeneralizedHeytingAlgebra α] [toOrderBot : OrderBot α] [toCompl : Compl α] (himp_bot : ∀ (a : α), a ⇨ ⊥ = aᶜ) : HeytingAlgebra α
• le_compl_self 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] {a : α} : a ≤ aᶜ ↔ a = ⊥
• lt_compl_self 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] {a : α} [Nontrivial α] : a < aᶜ ↔ a = ⊥
• compl_bot 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] : ⊥ᶜ = ⊤
• compl_top 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] : ⊤ᶜ = ⊥
• hnot_bot 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [CoheytingAlgebra α] : ￢⊥ = ⊤
• hnot_top 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [CoheytingAlgebra α] : ￢⊤ = ⊥
• bot_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] (a : α) : ⊥ ⇨ a = ⊤
• sdiff_top 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [CoheytingAlgebra α] (a : α) : a \ ⊤ = ⊥
• compl_unique 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] {a b : α} (h₀ : a ⊓ b = ⊥) (h₁ : a ⊔ b = ⊤) : aᶜ = b
• Function.Injective.generalizedCoheytingAlgebra 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} {β : Type u_3} [Max α] [Min α] [LE α] [LT α] [Bot α] [SDiff α] [GeneralizedCoheytingAlgebra β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_bot : f ⊥ = ⊥) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) : GeneralizedCoheytingAlgebra α
• Function.Injective.coheytingAlgebra 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} {β : Type u_3} [Min α] [Max α] [LE α] [LT α] [Bot α] [Top α] [HNot α] [SDiff α] [CoheytingAlgebra β] (f : α → β) (hf : Function.Injective f) (le : ∀ {y x : α}, f y ≤ f x ↔ y ≤ x) (lt : ∀ {y x : α}, f y < f x ↔ y < x) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_hnot : ∀ (a : α), f (￢a) = ￢f a) (map_sdiff : ∀ (b a : α), f (b \ a) = f b \ f a) : CoheytingAlgebra α
• Function.Injective.heytingAlgebra 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} {β : Type u_3} [Max α] [Min α] [LE α] [LT α] [Top α] [Bot α] [Compl α] [HImp α] [HeytingAlgebra β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) : HeytingAlgebra α
• Function.Injective.biheytingAlgebra 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} {β : Type u_3} [Max α] [Min α] [LE α] [LT α] [Top α] [Bot α] [Compl α] [HNot α] [HImp α] [SDiff α] [BiheytingAlgebra β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_hnot : ∀ (a : α), f (￢a) = ￢f a) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) : BiheytingAlgebra α
• BooleanAlgebra.bot_le 📋 Mathlib.Order.BooleanAlgebra.Defs
  {α : Type u} [self : BooleanAlgebra α] (a : α) : ⊥ ≤ a
• BooleanAlgebra.inf_compl_le_bot 📋 Mathlib.Order.BooleanAlgebra.Defs
  {α : Type u} [self : BooleanAlgebra α] (x : α) : x ⊓ xᶜ ≤ ⊥
• GeneralizedBooleanAlgebra.inf_inf_sdiff 📋 Mathlib.Order.BooleanAlgebra.Defs
  {α : Type u} [self : GeneralizedBooleanAlgebra α] (a b : α) : a ⊓ b ⊓ a \ b = ⊥
• GeneralizedBooleanAlgebra.mk 📋 Mathlib.Order.BooleanAlgebra.Defs
  {α : Type u} [toDistribLattice : DistribLattice α] [toSDiff : SDiff α] [toBot : Bot α] (sup_inf_sdiff : ∀ (a b : α), a ⊓ b ⊔ a \ b = a) (inf_inf_sdiff : ∀ (a b : α), a ⊓ b ⊓ a \ b = ⊥) : GeneralizedBooleanAlgebra α
• BooleanAlgebra.mk 📋 Mathlib.Order.BooleanAlgebra.Defs
  {α : Type u} [toDistribLattice : DistribLattice α] [toCompl : Compl α] [toSDiff : SDiff α] [toHImp : HImp α] [toTop : Top α] [toBot : Bot α] (inf_compl_le_bot : ∀ (x : α), x ⊓ xᶜ ≤ ⊥) (top_le_sup_compl : ∀ (x : α), ⊤ ≤ x ⊔ xᶜ) (le_top : ∀ (a : α), a ≤ ⊤) (bot_le : ∀ (a : α), ⊥ ≤ a) (sdiff_eq : ∀ (x y : α), x \ y = x ⊓ yᶜ := by aesop) (himp_eq : ∀ (x y : α), x ⇨ y = y ⊔ xᶜ := by aesop) : BooleanAlgebra α
• compl_eq_bot 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x : α} [BooleanAlgebra α] : xᶜ = ⊥ ↔ x = ⊤
• compl_eq_top 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x : α} [BooleanAlgebra α] : xᶜ = ⊤ ↔ x = ⊥
• inf_compl_eq_bot' 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x : α} [BooleanAlgebra α] : x ⊓ xᶜ = ⊥
• inf_sdiff_self_left 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : y \ x ⊓ x = ⊥
• inf_sdiff_self_right 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : x ⊓ y \ x = ⊥
• sdiff_eq_right 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : x \ y = y ↔ x = ⊥ ∧ y = ⊥
• sdiff_ne_right 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : x \ y ≠ y ↔ x ≠ ⊥ ∨ y ≠ ⊥
• le_sdiff_right 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : x ≤ y \ x ↔ x = ⊥
• sdiff_inf_sdiff 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] : x \ y ⊓ y \ x = ⊥
• inf_inf_sdiff 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} [GeneralizedBooleanAlgebra α] (x y : α) : x ⊓ y ⊓ x \ y = ⊥
• inf_sdiff_inf 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} [GeneralizedBooleanAlgebra α] (x y : α) : x \ y ⊓ (x ⊓ y) = ⊥
• sdiff_lt 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] (hx : y ≤ x) (hy : y ≠ ⊥) : x \ y < x
• sdiff_unique 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (s : x ⊓ y ⊔ z = x) (i : x ⊓ y ⊓ z = ⊥) : x \ y = z
• inf_sdiff_eq_bot_iff 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hz : z ≤ y) (hx : x ≤ y) : z ⊓ y \ x = ⊥ ↔ z ≤ x
• Function.Injective.generalizedBooleanAlgebra 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {β : Type u_1} [Max α] [Min α] [LE α] [LT α] [Bot α] [SDiff α] [GeneralizedBooleanAlgebra β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_bot : f ⊥ = ⊥) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) : GeneralizedBooleanAlgebra α
• Function.Injective.booleanAlgebra 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {β : Type u_1} [Max α] [Min α] [LE α] [LT α] [Top α] [Bot α] [Compl α] [SDiff α] [HImp α] [BooleanAlgebra β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) : BooleanAlgebra α
• symmDiff_eq_left 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedBooleanAlgebra α] {a b : α} : symmDiff a b = a ↔ b = ⊥
• symmDiff_eq_right 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedBooleanAlgebra α] {a b : α} : symmDiff a b = b ↔ a = ⊥
• bot_symmDiff 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) : symmDiff ⊥ a = a
• symmDiff_bot 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) : symmDiff a ⊥ = a
• symmDiff_self 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) : symmDiff a a = ⊥
• symmDiff_eq_bot 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b : α} : symmDiff a b = ⊥ ↔ a = b
• bihimp_bot 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [HeytingAlgebra α] (a : α) : bihimp a ⊥ = aᶜ
• bihimp_compl_self 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [HeytingAlgebra α] (a : α) : bihimp a aᶜ = ⊥
• bihimp_hnot_self 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [HeytingAlgebra α] (a : α) : bihimp a aᶜ = ⊥
• bot_bihimp 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [HeytingAlgebra α] (a : α) : bihimp ⊥ a = aᶜ
• compl_bihimp_self 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [HeytingAlgebra α] (a : α) : bihimp aᶜ a = ⊥
• bihimp_eq_bot 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [BooleanAlgebra α] (a b : α) : bihimp a b = ⊥ ↔ IsCompl a b
• IsCompl.bihimp_eq_bot 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [HeytingAlgebra α] {a b : α} (h : IsCompl a b) : bihimp a b = ⊥
• bot_eq_one 📋 Mathlib.Algebra.Order.IsBotOne
  {α : Type u_1} [PartialOrder α] [One α] [IsBotOneClass α] [OrderBot α] : ⊥ = 1
• bot_eq_zero 📋 Mathlib.Algebra.Order.IsBotOne
  {α : Type u_1} [PartialOrder α] [Zero α] [IsBotZeroClass α] [OrderBot α] : ⊥ = 0
• bot_eq_zero'' 📋 Mathlib.Algebra.Order.IsBotOne
  {α : Type u_1} [PartialOrder α] [Zero α] [IsBotZeroClass α] [OrderBot α] : ⊥ = 0

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