Loogle!

Result

Found 6617 declarations mentioning Top.top. Of these, only the first 200 are shown.

• Top.top 📋 Mathlib.Order.Notation
  {α : Type u_1} [self : Top α] : α
• Top.ext 📋 Mathlib.Order.Notation
  {α : Type u_1} {x y : Top α} (top : ⊤ = ⊤) : x = y
• Top.ext_iff 📋 Mathlib.Order.Notation
  {α : Type u_1} {x y : Top α} : x = y ↔ ⊤ = ⊤
• top_eq_true 📋 Mathlib.Order.BoundedOrder.Basic
  : ⊤ = true
• isTop_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [LE α] [OrderTop α] : IsTop ⊤
• OrderTop.mk 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [LE α] [toTop : Top α] (le_top : ∀ (a : α), a ≤ ⊤) : OrderTop α
• ULift.down_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Top α] : ⊤.down = ⊤
• le_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [LE α] [OrderTop α] {a : α} : a ≤ ⊤
• OrderTop.le_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} {inst✝ : LE α} [self : OrderTop α] (a : α) : a ≤ ⊤
• ULift.up_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Top α] : { down := ⊤ } = ⊤
• isMax_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Preorder α] [OrderTop α] : IsMax ⊤
• Prod.fst_top 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) (β : Type v) [Top α] [Top β] : ⊤.1 = ⊤
• Prod.snd_top 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) (β : Type v) [Top α] [Top β] : ⊤.2 = ⊤
• not_top_lt 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Preorder α] [OrderTop α] {a : α} : ¬⊤ < a
• Pi.top_apply 📋 Mathlib.Order.BoundedOrder.Basic
  {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → Top (α' i)] (i : ι) : ⊤ i = ⊤
• Pi.top_def 📋 Mathlib.Order.BoundedOrder.Basic
  {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → Top (α' i)] : ⊤ = fun x => ⊤
• Subtype.orderTop 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} {p : α → Prop} [LE α] [OrderTop α] (htop : p ⊤) : OrderTop { x // p x }
• ne_top_of_lt 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Preorder α] [OrderTop α] {a b : α} (h : a < b) : a ≠ ⊤
• LT.lt.ne_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Preorder α] [OrderTop α] {a b : α} (h : a < b) : a ≠ ⊤
• not_isMin_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] [Nontrivial α] : ¬IsMin ⊤
• lt_top_of_lt 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Preorder α] [OrderTop α] {a b : α} (h : a < b) : a < ⊤
• IsTop.rec 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [LE α] {P : (x : α) → IsTop x → Sort u_1} (h : [inst : OrderTop α] → P ⊤ ⋯) (x : α) (hx : IsTop x) : P x hx
• LT.lt.lt_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [Preorder α] [OrderTop α] {a b : α} (h : a < b) : a < ⊤
• IsMax.eq_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] {a : α} : IsMax a → a = ⊤
• IsTop.eq_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] {a : α} : IsTop a → a = ⊤
• isMax_iff_eq_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] {a : α} : IsMax a ↔ a = ⊤
• isTop_iff_eq_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] {a : α} : IsTop a ↔ a = ⊤
• Pi.top_comp 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Top γ] (x : α → β) : ⊤ ∘ x = ⊤
• not_isMax_iff_ne_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] {a : α} : ¬IsMax a ↔ a ≠ ⊤
• not_isTop_iff_ne_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] {a : α} : ¬IsTop 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 ⊤ = ⊥
• top_unique 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] {a : α} (h : ⊤ ≤ a) : a = ⊤
• Ne.lt_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] {a : α} (h : a ≠ ⊤) : a < ⊤
• Ne.lt_top' 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] {a : α} (h : ⊤ ≠ a) : a < ⊤
• OrderTop.lift 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} {β : Type v} [LE α] [Top α] [LE β] [OrderTop β] (f : α → β) (map_le : ∀ (a b : α), f a ≤ f b → a ≤ b) (map_top : f ⊤ = ⊤) : OrderTop α
• eq_top_iff 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] {a : α} : a = ⊤ ↔ ⊤ ≤ a
• eq_top_or_lt_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] (a : α) : a = ⊤ ∨ a < ⊤
• lt_top_iff_ne_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] {a : α} : a < ⊤ ↔ a ≠ ⊤
• top_le_iff 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] {a : α} : ⊤ ≤ a ↔ a = ⊤
• not_lt_top_iff 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] {a : α} : ¬a < ⊤ ↔ a = ⊤
• eq_top_mono 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] {a b : α} (h : a ≤ b) (h₂ : a = ⊤) : b = ⊤
• ne_top_of_le_ne_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] {a b : α} (hb : b ≠ ⊤) (hab : a ≤ b) : 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 α
• 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 α
• 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 α
• top_notMem_iff 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] {s : Set α} : ⊤ ∉ s ↔ ∀ x ∈ s, x < ⊤
• top_not_mem_iff 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} [PartialOrder α] [OrderTop α] {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 α
• OrderTop.ext_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u_1} {hA : PartialOrder α} (A : OrderTop α) {hB : PartialOrder α} (B : OrderTop α) (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) : ⊤ = ⊤
• eq_bot_of_bot_eq_top 📋 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 = ⊤
• Subtype.coe_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} {p : α → Prop} [PartialOrder α] [OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) : ↑⊤ = ⊤
• Subtype.mk_top 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} {p : α → Prop} [PartialOrder α] [OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) : ⟨⊤, htop⟩ = ⊤
• Subtype.mk_eq_top_iff 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} {p : α → Prop} [PartialOrder α] [OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) {x : α} (hx : p x) : ⟨x, hx⟩ = ⊤ ↔ x = ⊤
• Subtype.coe_eq_top_iff 📋 Mathlib.Order.BoundedOrder.Basic
  {α : Type u} {p : α → Prop} [PartialOrder α] [OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) {x : { x // p x }} : ↑x = ⊤ ↔ x = ⊤
• inf_top_eq 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u} [SemilatticeInf α] [OrderTop α] (a : α) : a ⊓ ⊤ = a
• top_inf_eq 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u} [SemilatticeInf α] [OrderTop α] (a : α) : ⊤ ⊓ a = a
• sup_top_eq 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u} [SemilatticeSup α] [OrderTop α] (a : α) : a ⊔ ⊤ = ⊤
• top_sup_eq 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u} [SemilatticeSup α] [OrderTop α] (a : α) : ⊤ ⊔ a = ⊤
• min_top_left 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u} [LinearOrder α] [OrderTop α] (a : α) : min ⊤ a = a
• min_top_right 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u} [LinearOrder α] [OrderTop α] (a : α) : min a ⊤ = a
• WellFoundedGT.induction_top 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u} [Preorder α] [WellFoundedGT α] [OrderTop α] {P : α → Prop} (hexists : ∃ M, P M) (hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M > N, P M) : P ⊤
• inf_eq_top_iff 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u} [SemilatticeInf α] [OrderTop α] {a b : α} : a ⊓ b = ⊤ ↔ a = ⊤ ∧ b = ⊤
• max_top_left 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u} [LinearOrder α] [OrderTop α] (a : α) : max ⊤ a = ⊤
• max_top_right 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u} [LinearOrder α] [OrderTop α] (a : α) : max a ⊤ = ⊤
• max_ne_top 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u} [LinearOrder α] [OrderTop α] {a b : α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : max a b ≠ ⊤
• max_eq_top 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u} [LinearOrder α] [OrderTop α] {a b : α} : max a b = ⊤ ↔ a = ⊤ ∨ b = ⊤
• min_eq_top 📋 Mathlib.Order.BoundedOrder.Lattice
  {α : Type u} [LinearOrder α] [OrderTop α] {a b : α} : min a b = ⊤ ↔ a = ⊤ ∧ b = ⊤
• codisjoint_top_left 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} : Codisjoint ⊤ a
• codisjoint_top_right 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} : Codisjoint a ⊤
• Codisjoint.eq_top_of_self 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} : Codisjoint a a → a = ⊤
• codisjoint_self 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} : Codisjoint a a ↔ a = ⊤
• Codisjoint.ne 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} (ha : a ≠ ⊤) (hab : Codisjoint a b) : a ≠ b
• Codisjoint.eq_top_of_ge 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} (hab : Codisjoint a b) : a ≤ b → b = ⊤
• Codisjoint.eq_top_of_le 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} (hab : Codisjoint a b) (h : b ≤ a) : a = ⊤
• isComplemented_top 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [Lattice α] [BoundedOrder α] : IsComplemented ⊤
• Codisjoint.eq_top 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} : Codisjoint a b → a ⊔ b = ⊤
• codisjoint_iff 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} : Codisjoint a b ↔ a ⊔ b = ⊤
• Codisjoint.eq_iff 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} (hab : Codisjoint a b) : a = b ↔ a = ⊤ ∧ b = ⊤
• Codisjoint.ne_iff 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} (hab : Codisjoint a b) : a ≠ b ↔ a ≠ ⊤ ∨ b ≠ ⊤
• Codisjoint.top_le 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} : Codisjoint a b → ⊤ ≤ a ⊔ b
• codisjoint_iff_le_sup 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} : Codisjoint 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.sup_eq_top 📋 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 ≠ ⊥
• Codisjoint.ne_bot_of_ne_top' 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a b : α} (h : Codisjoint a b) (hb : b ≠ ⊤) : a ≠ ⊥
• 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 = ⊤
• IsCompl.of_eq 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [Lattice α] [BoundedOrder α] {x y : α} (h₁ : x ⊓ y = ⊥) (h₂ : x ⊔ y = ⊤) : IsCompl x y
• Complementeds.coe_top 📋 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_top 📋 Mathlib.Order.Disjoint
  {α : Type u_1} [Lattice α] [BoundedOrder α] : ⟨⊤, ⋯⟩ = ⊤
• Prop.top_eq_true 📋 Mathlib.Order.PropInstances
  : ⊤ = True
• Prop.decidablePredTop 📋 Mathlib.Order.PropInstances
  {α : Type u} : DecidablePred ⊤
• Prop.decidableRelTop 📋 Mathlib.Order.PropInstances
  {α : Type u} : DecidableRel ⊤
• Set.setOf_top 📋 Mathlib.Data.Set.Basic
  {α : Type u} : {_x | ⊤} = Set.univ
• Set.instNonemptyTop 📋 Mathlib.Data.Set.Basic
  {α : Type u} [Nonempty α] : Nonempty ↑⊤
• Set.top_eq_univ 📋 Mathlib.Data.Set.Basic
  {α : Type u} : ⊤ = Set.univ
• Set.not_top_subset 📋 Mathlib.Data.Set.Basic
  {α : Type u} {s : Set α} : ¬⊤ ⊆ s ↔ ∃ a, a ∉ s
• GaloisConnection.u_l_top 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] [OrderTop α] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u (l ⊤) = ⊤
• GaloisConnection.u_top 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] [OrderTop α] [OrderTop β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u ⊤ = ⊤
• GaloisInsertion.l_top 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} {l : α → β} {u : β → α} [Preorder α] [PartialOrder β] [OrderTop α] [OrderTop β] (gi : GaloisInsertion l u) : l ⊤ = ⊤
• GaloisConnection.u_eq_top 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] [OrderTop α] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {x : β} : u x = ⊤ ↔ l ⊤ ≤ x
• PUnit.top_eq 📋 Mathlib.Order.Heyting.Basic
  : ⊤ = PUnit.unit
• himp_self 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} : a ⇨ a = ⊤
• top_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} : ⊤ ⇨ a = a
• top_sdiff' 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [CoheytingAlgebra α] (a : α) : ⊤ \ a = ￢a
• CoheytingAlgebra.top_sdiff 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_4} [self : CoheytingAlgebra α] (a : α) : ⊤ \ a = ￢a
• hnot_sup_self 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [CoheytingAlgebra α] (a : α) : ￢a ⊔ a = ⊤
• sup_hnot_self 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [CoheytingAlgebra α] (a : α) : a ⊔ ￢a = ⊤
• BiheytingAlgebra.top_sdiff 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_4} [self : BiheytingAlgebra α] (a : α) : ⊤ \ a = ￢a
• himp_eq_top_iff 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} : a ⇨ b = ⊤ ↔ a ≤ b
• himp_top 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} : a ⇨ ⊤ = ⊤
• CoheytingAlgebra.mk 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_4} [toGeneralizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α] [toOrderTop : OrderTop α] [toHNot : HNot α] (top_sdiff : ∀ (a : α), ⊤ \ a = ￢a) : CoheytingAlgebra α
• 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 \ ⊤ = ⊥
• BiheytingAlgebra.mk 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_4} [toHeytingAlgebra : HeytingAlgebra α] [toSDiff : SDiff α] [toHNot : HNot α] (sdiff_le_iff : ∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c) (top_sdiff : ∀ (a : α), ⊤ \ a = ￢a) : BiheytingAlgebra α
• compl_unique 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [HeytingAlgebra α] {a b : α} (h₀ : a ⊓ b = ⊥) (h₁ : a ⊔ b = ⊤) : aᶜ = b
• Function.Injective.generalizedHeytingAlgebra 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} {β : Type u_3} [Max α] [Min α] [Top α] [HImp α] [GeneralizedHeytingAlgebra β] (f : α → β) (hf : Function.Injective f) (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_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) : GeneralizedHeytingAlgebra α
• Function.Injective.coheytingAlgebra 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} {β : Type u_3} [Max α] [Min α] [Top α] [Bot α] [HNot α] [SDiff α] [CoheytingAlgebra β] (f : α → β) (hf : Function.Injective f) (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 : ∀ (a b : α), f (a \ b) = f a \ f b) : CoheytingAlgebra α
• Function.Injective.heytingAlgebra 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} {β : Type u_3} [Max α] [Min α] [Top α] [Bot α] [HasCompl α] [HImp α] [HeytingAlgebra β] (f : α → β) (hf : Function.Injective f) (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 α] [Top α] [Bot α] [HasCompl α] [HNot α] [HImp α] [SDiff α] [BiheytingAlgebra β] (f : α → β) (hf : Function.Injective f) (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.le_top 📋 Mathlib.Order.BooleanAlgebra.Defs
  {α : Type u} [self : BooleanAlgebra α] (a : α) : a ≤ ⊤
• BooleanAlgebra.top_le_sup_compl 📋 Mathlib.Order.BooleanAlgebra.Defs
  {α : Type u} [self : BooleanAlgebra α] (x : α) : ⊤ ≤ x ⊔ xᶜ
• BooleanAlgebra.mk 📋 Mathlib.Order.BooleanAlgebra.Defs
  {α : Type u} [toDistribLattice : DistribLattice α] [toHasCompl : HasCompl α] [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 α
• top_sdiff 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x : α} [BooleanAlgebra α] : ⊤ \ x = xᶜ
• 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 = ⊥
• compl_sup_eq_top 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x : α} [BooleanAlgebra α] : xᶜ ⊔ x = ⊤
• sup_compl_eq_top 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x : α} [BooleanAlgebra α] : x ⊔ xᶜ = ⊤
• himp_eq_left 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [BooleanAlgebra α] : x ⇨ y = x ↔ x = ⊤ ∧ y = ⊤
• himp_ne_right 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [BooleanAlgebra α] : x ⇨ y ≠ x ↔ x ≠ ⊤ ∨ y ≠ ⊤
• compl_le_self 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x : α} [BooleanAlgebra α] : xᶜ ≤ x ↔ x = ⊤
• compl_lt_self 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x : α} [BooleanAlgebra α] [Nontrivial α] : xᶜ < x ↔ x = ⊤
• himp_le_left 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {x y : α} [BooleanAlgebra α] : x ⇨ y ≤ x ↔ x = ⊤
• Function.Injective.booleanAlgebra 📋 Mathlib.Order.BooleanAlgebra.Basic
  {α : Type u} {β : Type u_1} [Max α] [Min α] [Top α] [Bot α] [HasCompl α] [SDiff α] [HImp α] [BooleanAlgebra β] (f : α → β) (hf : Function.Injective f) (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 α
• compl_symmDiff_self 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [BooleanAlgebra α] (a : α) : symmDiff aᶜ a = ⊤
• symmDiff_compl_self 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [BooleanAlgebra α] (a : α) : symmDiff a aᶜ = ⊤
• symmDiff_top 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [BooleanAlgebra α] (a : α) : symmDiff a ⊤ = aᶜ
• top_symmDiff 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [BooleanAlgebra α] (a : α) : symmDiff ⊤ a = aᶜ
• bihimp_eq_left 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [BooleanAlgebra α] {a b : α} : bihimp a b = a ↔ b = ⊤
• bihimp_eq_right 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [BooleanAlgebra α] {a b : α} : bihimp a b = b ↔ a = ⊤
• bihimp_self 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) : bihimp a a = ⊤
• bihimp_top 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) : bihimp a ⊤ = a
• top_bihimp 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) : bihimp ⊤ a = a
• bihimp_eq_top 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} : bihimp a b = ⊤ ↔ a = b
• hnot_symmDiff_self 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [CoheytingAlgebra α] (a : α) : symmDiff (￢a) a = ⊤
• symmDiff_hnot_self 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [CoheytingAlgebra α] (a : α) : symmDiff a (￢a) = ⊤
• symmDiff_top' 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [CoheytingAlgebra α] (a : α) : symmDiff a ⊤ = ￢a
• top_symmDiff' 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [CoheytingAlgebra α] (a : α) : symmDiff ⊤ a = ￢a
• symmDiff_eq_top 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [BooleanAlgebra α] (a b : α) : symmDiff a b = ⊤ ↔ IsCompl a b
• IsCompl.symmDiff_eq_top 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} [CoheytingAlgebra α] {a b : α} (h : IsCompl a b) : symmDiff a b = ⊤
• OrderIso.map_top 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} [LE α] [PartialOrder β] [OrderTop α] [OrderTop β] (f : α ≃o β) : f ⊤ = ⊤
• WithTop.recTopCoe 📋 Mathlib.Order.TypeTags
  {α : Type u_1} {C : WithTop α → Sort u_2} (top : C ⊤) (coe : (a : α) → C ↑a) (n : WithTop α) : C n
• WithTop.recTopCoe_coe 📋 Mathlib.Order.TypeTags
  {α : Type u_1} {C : WithTop α → Sort u_2} (d : C ⊤) (f : (a : α) → C ↑a) (x : α) : WithTop.recTopCoe d f ↑x = f x
• WithTop.recTopCoe_top 📋 Mathlib.Order.TypeTags
  {α : Type u_1} {C : WithTop α → Sort u_2} (d : C ⊤) (f : (a : α) → C ↑a) : WithTop.recTopCoe d f ⊤ = d
• WithTop.none_eq_top 📋 Mathlib.Order.WithBot
  {α : Type u_1} : none = ⊤
• WithTop.coe_ne_top 📋 Mathlib.Order.WithBot
  {α : Type u_1} {a : α} : ↑a ≠ ⊤
• WithTop.top_ne_coe 📋 Mathlib.Order.WithBot
  {α : Type u_1} {a : α} : ⊤ ≠ ↑a
• WithTop.untop 📋 Mathlib.Order.WithBot
  {α : Type u_1} (x : WithTop α) : x ≠ ⊤ → α
• WithTop.untop'_top 📋 Mathlib.Order.WithBot
  {α : Type u_5} (d : α) : WithTop.untopD d ⊤ = d
• WithTop.untopD_top 📋 Mathlib.Order.WithBot
  {α : Type u_5} (d : α) : WithTop.untopD d ⊤ = d
• Equiv.withTopSubtypeNe 📋 Mathlib.Order.WithBot
  {α : Type u_1} : { y // y ≠ ⊤ } ≃ α
• WithBot.coe_top 📋 Mathlib.Order.WithBot
  {α : Type u_1} [Top α] : ↑⊤ = ⊤
• WithTop.canLift 📋 Mathlib.Order.WithBot
  {α : Type u_1} : CanLift (WithTop α) α WithTop.some fun r => r ≠ ⊤
• WithTop.coe_lt_top 📋 Mathlib.Order.WithBot
  {α : Type u_1} [LT α] (a : α) : ↑a < ⊤
• WithTop.not_top_lt 📋 Mathlib.Order.WithBot
  {α : Type u_1} [LT α] (a : WithTop α) : ¬⊤ < a
• WithTop.not_top_le_coe 📋 Mathlib.Order.WithBot
  {α : Type u_1} [LE α] (a : α) : ¬⊤ ≤ ↑a
• WithTop.eq_top_iff_forall_ne 📋 Mathlib.Order.WithBot
  {α : Type u_1} {x : WithTop α} : x = ⊤ ↔ ∀ (a : α), ↑a ≠ x
• WithTop.forall 📋 Mathlib.Order.WithBot
  {α : Type u_1} {p : WithTop α → Prop} : (∀ (x : WithTop α), p x) ↔ p ⊤ ∧ ∀ (x : α), p ↑x
• WithTop.forall_ne_iff_eq_top 📋 Mathlib.Order.WithBot
  {α : Type u_1} {x : WithTop α} : x = ⊤ ↔ ∀ (a : α), ↑a ≠ x
• WithTop.map_top 📋 Mathlib.Order.WithBot
  {α : Type u_1} {β : Type u_2} (f : α → β) : WithTop.map f ⊤ = ⊤
• WithTop.coe_untop 📋 Mathlib.Order.WithBot
  {α : Type u_1} (x : WithTop α) (hx : x ≠ ⊤) : ↑(x.untop hx) = x
• WithBot.coe_eq_top 📋 Mathlib.Order.WithBot
  {α : Type u_1} [Top α] {a : α} : ↑a = ⊤ ↔ a = ⊤
• WithBot.top_eq_coe 📋 Mathlib.Order.WithBot
  {α : Type u_1} [Top α] {a : α} : ⊤ = ↑a ↔ ⊤ = a
• WithTop.ne_top_iff_exists 📋 Mathlib.Order.WithBot
  {α : Type u_1} {x : WithTop α} : x ≠ ⊤ ↔ ∃ a, ↑a = x
• WithTop.exists 📋 Mathlib.Order.WithBot
  {α : Type u_1} {p : WithTop α → Prop} : (∃ x, p x) ↔ p ⊤ ∨ ∃ x, p ↑x
• WithTop.untop_coe 📋 Mathlib.Order.WithBot
  {α : Type u_1} (x : α) (h : ↑x ≠ ⊤ := ⋯) : (↑x).untop h = x
• WithTop.lt_top_iff_ne_top 📋 Mathlib.Order.WithBot
  {α : Type u_1} [LT α] {x : WithTop α} : x < ⊤ ↔ x ≠ ⊤
• WithTop.map₂_top_left 📋 Mathlib.Order.WithBot
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (b : WithTop β) : WithTop.map₂ f ⊤ b = ⊤
• WithTop.map₂_top_right 📋 Mathlib.Order.WithBot
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : WithTop α) : WithTop.map₂ f a ⊤ = ⊤
• WithTop.top_le_iff 📋 Mathlib.Order.WithBot
  {α : Type u_1} [LE α] {a : WithTop α} : ⊤ ≤ a ↔ a = ⊤

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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.

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.

This is Loogle revision ff04530 serving mathlib revision fe81dd4