Loogle!

Result

Found 703 declarations mentioning ULift. Of these, only the first 200 are shown.

ULift 📋 Init.Prelude
(α : Type s) : Type (max s r)
ULift.down 📋 Init.Prelude
{α : Type s} (self : ULift.{r, s} α) : α
ULift.up 📋 Init.Prelude
{α : Type s} (down : α) : ULift.{r, s} α
ULift.up_down 📋 Init.Prelude
{α : Type u} (b : ULift.{v, u} α) : { down := b.down } = b
ULift.up.sizeOf_spec 📋 Init.SizeOf
{α : Type s} [SizeOf α] (down : α) : sizeOf { down := down } = 1 + sizeOf down
ULift.up.injEq 📋 Init.Core
{α : Type s} (down down✝ : α) : ({ down := down } = { down := down✝ }) = (down = down✝)
instReprULift 📋 Init.Data.Repr
{α : Type u_1} [Repr α] : Repr (ULift.{v, u_1} α)
instToStringULift 📋 Init.Data.ToString.Basic
{α : Type u} [ToString α] : ToString (ULift.{v, u} α)
instDecidableEqULift 📋 Init.Data.ULift
{α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (ULift.{u_2, u_1} α✝)
instSubsingletonULift 📋 Init.Data.ULift
{α : Type u_1} [Subsingleton α] : Subsingleton (ULift.{u_2, u_1} α)
MLList.isEmpty 📋 Batteries.Data.MLList.Basic
{m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (xs : MLList m α) : m (ULift.{u_1, 0} Bool)
MLList.filterM 📋 Batteries.Data.MLList.Basic
{m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (p : α → m (ULift.{u_1, 0} Bool)) (L : MLList m α) : MLList m α
MLList.takeUpToFirstM 📋 Batteries.Data.MLList.Basic
{m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (L : MLList m α) (f : α → m (ULift.{u_1, 0} Bool)) : MLList m α
MLList.takeWhileM 📋 Batteries.Data.MLList.Basic
{m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (f : α → m (ULift.{u_1, 0} Bool)) (L : MLList m α) : MLList m α
Nondet.filterM 📋 Batteries.Control.Nondet.Basic
{σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (p : α → m (ULift.{0, 0} Bool)) (L : Nondet m α) : Nondet m α
nonempty_ulift 📋 Mathlib.Logic.Nonempty
{α : Type u_1} : Nonempty (ULift.{u_4, u_1} α) ↔ Nonempty α
isEmpty_ulift 📋 Mathlib.Logic.IsEmpty
{α : Type u_4} : IsEmpty (ULift.{u_5, u_4} α) ↔ IsEmpty α
Equiv.ulift 📋 Mathlib.Logic.Equiv.Defs
{α : Type v} : ULift.{u, v} α ≃ α
Equiv.sigmaULiftPLiftEquivSubtype 📋 Mathlib.Logic.Equiv.Defs
{α : Type v} (P : α → Prop) : (i : α) × ULift.{u_1, 0} (PLift (P i)) ≃ Subtype P
Equiv.ulift_apply 📋 Mathlib.Logic.Equiv.Defs
{α : Type v} : ⇑Equiv.ulift = ULift.down
Aesop.filterDiscrTreeM 📋 Aesop.Util.Basic
{m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type} [Monad m] [Inhabited σ] (p : α → m (ULift.{u_1, 0} Bool)) (f : σ → α → m σ) (init : σ) (t : Lean.Meta.DiscrTree α) : m (Lean.Meta.DiscrTree α × σ)
Mathlib.instToExprULiftOfToLevel_mathlib 📋 Mathlib.Tactic.ToExpr
{α✝ : Type s} [Lean.ToExpr α✝] [Lean.ToLevel] [Lean.ToLevel] : Lean.ToExpr (ULift.{r, s} α✝)
ULift.down_injective 📋 Mathlib.Logic.Function.ULift
{α : Type u_1} : Function.Injective ULift.down
ULift.down_inj 📋 Mathlib.Logic.Function.ULift
{α : Type u_1} {a b : ULift.{u_2, u_1} α} : a.down = b.down ↔ a = b
ULift.instBEq_mathlib 📋 Mathlib.Order.ULift
{α : Type u} [BEq α] : BEq (ULift.{v, u} α)
ULift.instHasCompl 📋 Mathlib.Order.ULift
{α : Type u} [HasCompl α] : HasCompl (ULift.{v, u} α)
ULift.instLE_mathlib 📋 Mathlib.Order.ULift
{α : Type u} [LE α] : LE (ULift.{v, u} α)
ULift.instLT_mathlib 📋 Mathlib.Order.ULift
{α : Type u} [LT α] : LT (ULift.{v, u} α)
ULift.instMax_mathlib 📋 Mathlib.Order.ULift
{α : Type u} [Max α] : Max (ULift.{v, u} α)
ULift.instMin_mathlib 📋 Mathlib.Order.ULift
{α : Type u} [Min α] : Min (ULift.{v, u} α)
ULift.instOrd_mathlib 📋 Mathlib.Order.ULift
{α : Type u} [Ord α] : Ord (ULift.{v, u} α)
ULift.instPartialOrder 📋 Mathlib.Order.ULift
{α : Type u} [PartialOrder α] : PartialOrder (ULift.{v, u} α)
ULift.instPreorder 📋 Mathlib.Order.ULift
{α : Type u} [Preorder α] : Preorder (ULift.{v, u} α)
ULift.instSDiff_mathlib 📋 Mathlib.Order.ULift
{α : Type u} [SDiff α] : SDiff (ULift.{v, u} α)
ULift.instOrientedOrd_mathlib 📋 Mathlib.Order.ULift
{α : Type u} [Ord α] [inst : Batteries.OrientedOrd α] : Batteries.OrientedOrd (ULift.{v, u} α)
ULift.instTransOrd_mathlib 📋 Mathlib.Order.ULift
{α : Type u} [Ord α] [inst : Batteries.TransOrd α] : Batteries.TransOrd (ULift.{v, u} α)
ULift.instBEqOrd_mathlib 📋 Mathlib.Order.ULift
{α : Type u} [BEq α] [Ord α] [inst : Batteries.BEqOrd α] : Batteries.BEqOrd (ULift.{v, u} α)
ULift.instLEOrd_mathlib 📋 Mathlib.Order.ULift
{α : Type u} [LE α] [Ord α] [inst : Batteries.LEOrd α] : Batteries.LEOrd (ULift.{v, u} α)
ULift.instLTOrd_mathlib 📋 Mathlib.Order.ULift
{α : Type u} [LT α] [Ord α] [inst : Batteries.LTOrd α] : Batteries.LTOrd (ULift.{v, u} α)
ULift.down_compl 📋 Mathlib.Order.ULift
{α : Type u} [HasCompl α] (a : ULift.{u_1, u} α) : aᶜ.down = a.downᶜ
ULift.up_compl 📋 Mathlib.Order.ULift
{α : Type u} [HasCompl α] (a : α) : { down := aᶜ } = { down := a }ᶜ
ULift.up_le 📋 Mathlib.Order.ULift
{α : Type u} [LE α] {a b : α} : { down := a } ≤ { down := b } ↔ a ≤ b
ULift.up_lt 📋 Mathlib.Order.ULift
{α : Type u} [LT α] {a b : α} : { down := a } < { down := b } ↔ a < b
ULift.up_beq 📋 Mathlib.Order.ULift
{α : Type u} [BEq α] (a b : α) : ({ down := a } == { down := b }) = (a == b)
ULift.up_compare 📋 Mathlib.Order.ULift
{α : Type u} [Ord α] (a b : α) : compare { down := a } { down := b } = compare a b
ULift.down_le 📋 Mathlib.Order.ULift
{α : Type u} [LE α] {a b : ULift.{u_1, u} α} : a.down ≤ b.down ↔ a ≤ b
ULift.down_lt 📋 Mathlib.Order.ULift
{α : Type u} [LT α] {a b : ULift.{u_1, u} α} : a.down < b.down ↔ a < b
ULift.down_beq 📋 Mathlib.Order.ULift
{α : Type u} [BEq α] (a b : ULift.{u_1, u} α) : (a.down == b.down) = (a == b)
ULift.down_compare 📋 Mathlib.Order.ULift
{α : Type u} [Ord α] (a b : ULift.{u_1, u} α) : compare a.down b.down = compare a b
ULift.up_inf 📋 Mathlib.Order.ULift
{α : Type u} [Min α] (a b : α) : { down := a ⊓ b } = { down := a } ⊓ { down := b }
ULift.up_sdiff 📋 Mathlib.Order.ULift
{α : Type u} [SDiff α] (a b : α) : { down := a \ b } = { down := a } \ { down := b }
ULift.up_sup 📋 Mathlib.Order.ULift
{α : Type u} [Max α] (a b : α) : { down := a ⊔ b } = { down := a } ⊔ { down := b }
ULift.down_inf 📋 Mathlib.Order.ULift
{α : Type u} [Min α] (a b : ULift.{u_1, u} α) : (a ⊓ b).down = a.down ⊓ b.down
ULift.down_sdiff 📋 Mathlib.Order.ULift
{α : Type u} [SDiff α] (a b : ULift.{u_1, u} α) : (a \ b).down = a.down \ b.down
ULift.down_sup 📋 Mathlib.Order.ULift
{α : Type u} [Max α] (a b : ULift.{u_1, u} α) : (a ⊔ b).down = a.down ⊔ b.down
ULift.instLawfulOrd_mathlib 📋 Mathlib.Order.ULift
{α : Type u} [LE α] [LT α] [BEq α] [Ord α] [inst : Batteries.LawfulOrd α] : Batteries.LawfulOrd (ULift.{v, u} α)
ULift.instBot 📋 Mathlib.Order.BoundedOrder.Basic
{α : Type u} [Bot α] : Bot (ULift.{v, u} α)
ULift.instTop 📋 Mathlib.Order.BoundedOrder.Basic
{α : Type u} [Top α] : Top (ULift.{v, u} α)
ULift.instBoundedOrder 📋 Mathlib.Order.BoundedOrder.Basic
{α : Type u} [LE α] [BoundedOrder α] : BoundedOrder (ULift.{v, u} α)
ULift.instOrderBot 📋 Mathlib.Order.BoundedOrder.Basic
{α : Type u} [LE α] [OrderBot α] : OrderBot (ULift.{v, u} α)
ULift.instOrderTop 📋 Mathlib.Order.BoundedOrder.Basic
{α : Type u} [LE α] [OrderTop α] : OrderTop (ULift.{v, u} α)
ULift.down_bot 📋 Mathlib.Order.BoundedOrder.Basic
{α : Type u} [Bot α] : ⊥.down = ⊥
ULift.down_top 📋 Mathlib.Order.BoundedOrder.Basic
{α : Type u} [Top α] : ⊤.down = ⊤
ULift.up_bot 📋 Mathlib.Order.BoundedOrder.Basic
{α : Type u} [Bot α] : { down := ⊥ } = ⊥
ULift.up_top 📋 Mathlib.Order.BoundedOrder.Basic
{α : Type u} [Top α] : { down := ⊤ } = ⊤
ULift.instDistribLattice 📋 Mathlib.Order.Lattice
{α : Type u} [DistribLattice α] : DistribLattice (ULift.{v, u} α)
ULift.instLattice 📋 Mathlib.Order.Lattice
{α : Type u} [Lattice α] : Lattice (ULift.{v, u} α)
ULift.instLinearOrder 📋 Mathlib.Order.Lattice
{α : Type u} [LinearOrder α] : LinearOrder (ULift.{v, u} α)
ULift.instSemilatticeInf 📋 Mathlib.Order.Lattice
{α : Type u} [SemilatticeInf α] : SemilatticeInf (ULift.{v, u} α)
ULift.instSemilatticeSup 📋 Mathlib.Order.Lattice
{α : Type u} [SemilatticeSup α] : SemilatticeSup (ULift.{v, u} α)
Equiv.ulift_symm_down 📋 Mathlib.Logic.Equiv.Basic
{α : Type v} (x : α) : (Equiv.ulift.symm x).down = x
Plausible.Rand.down 📋 Plausible.Random
{α : Type u} {g : Type} [RandomGen g] (x : Plausible.RandG g (ULift.{v, u} α)) : Plausible.RandG g α
Plausible.Rand.up 📋 Plausible.Random
{α : Type u} {g : Type} [RandomGen g] (x : Plausible.RandG g α) : Plausible.RandG g (ULift.{v, u} α)
Plausible.RandT.down 📋 Plausible.Random
{α : Type u} {m : Type (max u v) → Type w} {m' : Type u → Type w'} {g : Type} [RandomGen g] [Monad m] [Monad m'] (m_down : {α : Type u} → m (ULift.{v, u} α) → m' α) (x : Plausible.RandGT g m (ULift.{v, u} α)) : Plausible.RandGT g m' α
Plausible.RandT.up 📋 Plausible.Random
{α : Type u} {m : Type u → Type w} {m' : Type (max u v) → Type w'} {g : Type} [RandomGen g] [Monad m] [Monad m'] (m_up : {α : Type u} → m α → m' (ULift.{v, u} α)) (x : Plausible.RandGT g m α) : Plausible.RandGT g m' (ULift.{v, u} α)
Plausible.Gen.down 📋 Plausible.Gen
{α : Type u_1} (x : Plausible.Gen (ULift.{v, u_1} α)) : Plausible.Gen α
Plausible.Gen.up 📋 Plausible.Gen
{α : Type u} (x : Plausible.Gen α) : Plausible.Gen (ULift.{v, u} α)
Plausible.ULift.sampleableExt 📋 Plausible.Sampleable
{α : Type u_1} [Plausible.SampleableExt α] : Plausible.SampleableExt (ULift.{u_3, u_1} α)
Plausible.ULift.shrinkable 📋 Plausible.Sampleable
{α : Type u_1} [Plausible.Shrinkable α] : Plausible.Shrinkable (ULift.{u_2, u_1} α)
Plausible.Testable.forallTypesULiftTestable 📋 Plausible.Testable
{var : String} {f : Type u → Prop} [Plausible.Testable (f (ULift.{u, 0} ℤ))] : Plausible.Testable (Plausible.NamedBinder var (∀ (x : Type u), f x))
RelIso.IsWellOrder.ulift 📋 Mathlib.Order.RelIso.Basic
{α : Type u} (r : α → α → Prop) [IsWellOrder α r] : IsWellOrder (ULift.{u_5, u} α) (ULift.down ⁻¹'o r)
OrderHom.uliftMap 📋 Mathlib.Order.Hom.Basic
{α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) : ULift.{u_8, u_2} α →o ULift.{u_9, u_3} β
OrderHom.uliftMap_coe_down 📋 Mathlib.Order.Hom.Basic
{α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : α →o β) (i : ULift.{u_8, u_2} α) : (f.uliftMap i).down = f i.down
ULift.instMonad_mathlib 📋 Mathlib.Control.ULift
: Monad ULift.{u_2, u_1}
ULift.instLawfulMonad_mathlib 📋 Mathlib.Control.ULift
: LawfulMonad ULift.{u_2, u_1}
ULift.pure 📋 Mathlib.Control.ULift
{α : Type u} : α → ULift.{u_1, u} α
ULift.instLawfulApplicative_mathlib 📋 Mathlib.Control.ULift
: LawfulApplicative ULift.{u_2, u_1}
ULift.instLawfulFunctor_mathlib 📋 Mathlib.Control.ULift
: LawfulFunctor ULift.{u_2, u_1}
ULift.map 📋 Mathlib.Control.ULift
{α : Type u} {β : Type v} (f : α → β) (a : ULift.{u', u} α) : ULift.{v', v} β
ULift.bind 📋 Mathlib.Control.ULift
{α : Type u} {β : Type v} (a : ULift.{u_1, u} α) (f : α → ULift.{u_2, v} β) : ULift.{u_2, v} β
ULift.pure.eq_1 📋 Mathlib.Control.ULift
{α : Type u} : ULift.pure = ULift.up
ULift.seq 📋 Mathlib.Control.ULift
{α : Type u_1} {β : Type u_2} (f : ULift.{u_3, max u_1 u_2} (α → β)) (x : Unit → ULift.{u_4, u_1} α) : ULift.{u, u_2} β
ULift.rec.constant 📋 Mathlib.Control.ULift
{α : Type u} {β : Sort v} (b : β) : (ULift.rec fun x => b) = fun x => b
ULift.bind_up 📋 Mathlib.Control.ULift
{α : Type u} {β : Type v} (a : α) (f : α → ULift.{u_1, v} β) : { down := a }.bind f = f a
ULift.map_up 📋 Mathlib.Control.ULift
{α : Type u} {β : Type v} (f : α → β) (a : α) : ULift.map f { down := a } = { down := f a }
ULift.seq_up 📋 Mathlib.Control.ULift
{α : Type u} {β : Type v} (f : α → β) (x : α) : ({ down := f }.seq fun x_1 => { down := x }) = { down := f x }
ULift.instDecidableEq_mathlib 📋 Mathlib.Data.ULift
{α : Type u} [DecidableEq α] : DecidableEq (ULift.{u_1, u} α)
ULift.instIsEmpty 📋 Mathlib.Data.ULift
{α : Type u} [IsEmpty α] : IsEmpty (ULift.{u_1, u} α)
ULift.instNonempty_mathlib 📋 Mathlib.Data.ULift
{α : Type u} [Nonempty α] : Nonempty (ULift.{u_1, u} α)
ULift.instSubsingleton_mathlib 📋 Mathlib.Data.ULift
{α : Type u} [Subsingleton α] : Subsingleton (ULift.{u_1, u} α)
ULift.instUnique 📋 Mathlib.Data.ULift
{α : Type u} [Unique α] : Unique (ULift.{u_1, u} α)
ULift.down_bijective 📋 Mathlib.Data.ULift
{α : Type u} : Function.Bijective ULift.down
ULift.down_surjective 📋 Mathlib.Data.ULift
{α : Type u} : Function.Surjective ULift.down
ULift.up_bijective 📋 Mathlib.Data.ULift
{α : Type u} : Function.Bijective ULift.up
ULift.up_injective 📋 Mathlib.Data.ULift
{α : Type u} : Function.Injective ULift.up
ULift.up_surjective 📋 Mathlib.Data.ULift
{α : Type u} : Function.Surjective ULift.up
ULift.forall 📋 Mathlib.Data.ULift
{α : Type u} {p : ULift.{u_1, u} α → Prop} : (∀ (x : ULift.{u_1, u} α), p x) ↔ ∀ (x : α), p { down := x }
ULift.up_inj 📋 Mathlib.Data.ULift
{α : Type u} {x y : α} : { down := x } = { down := y } ↔ x = y
ULift.ext 📋 Mathlib.Data.ULift
{α : Type u} (x y : ULift.{u_1, u} α) (h : x.down = y.down) : x = y
ULift.map_bijective 📋 Mathlib.Data.ULift
{α : Type u} {β : Type v} {f : α → β} : Function.Bijective (ULift.map f) ↔ Function.Bijective f
ULift.map_injective 📋 Mathlib.Data.ULift
{α : Type u} {β : Type v} {f : α → β} : Function.Injective (ULift.map f) ↔ Function.Injective f
ULift.map_surjective 📋 Mathlib.Data.ULift
{α : Type u} {β : Type v} {f : α → β} : Function.Surjective (ULift.map f) ↔ Function.Surjective f
ULift.exists 📋 Mathlib.Data.ULift
{α : Type u} {p : ULift.{u_1, u} α → Prop} : (∃ x, p x) ↔ ∃ x, p { down := x }
ULift.ext_iff 📋 Mathlib.Data.ULift
{α : Type u} {x y : ULift.{u_1, u} α} : x = y ↔ x.down = y.down
ULift.rec_update 📋 Mathlib.Data.ULift
{α : Type u} {β : ULift.{u_2, u} α → Type u_1} [DecidableEq α] (f : (a : α) → β { down := a }) (a : α) (x : β { down := a }) : (fun t => ULift.rec (Function.update f a x) t) = Function.update (fun t => ULift.rec f t) { down := a } x
iInf_ulift 📋 Mathlib.Order.CompleteLattice.Basic
{α : Type u_1} {ι : Type u_8} [InfSet α] (f : ULift.{u_9, u_8} ι → α) : ⨅ i, f i = ⨅ i, f { down := i }
iSup_ulift 📋 Mathlib.Order.CompleteLattice.Basic
{α : Type u_1} {ι : Type u_8} [SupSet α] (f : ULift.{u_9, u_8} ι → α) : ⨆ i, f i = ⨆ i, f { down := i }
ULift.infSet 📋 Mathlib.Order.CompleteLattice.Lemmas
{α : Type u_1} [InfSet α] : InfSet (ULift.{v, u_1} α)
ULift.instCompleteLattice 📋 Mathlib.Order.CompleteLattice.Lemmas
{α : Type u_1} [CompleteLattice α] : CompleteLattice (ULift.{v, u_1} α)
ULift.supSet 📋 Mathlib.Order.CompleteLattice.Lemmas
{α : Type u_1} [SupSet α] : SupSet (ULift.{v, u_1} α)
ULift.down_sInf 📋 Mathlib.Order.CompleteLattice.Lemmas
{α : Type u_1} [InfSet α] (s : Set (ULift.{v, u_1} α)) : (sInf s).down = sInf (ULift.up ⁻¹' s)
ULift.down_sSup 📋 Mathlib.Order.CompleteLattice.Lemmas
{α : Type u_1} [SupSet α] (s : Set (ULift.{v, u_1} α)) : (sSup s).down = sSup (ULift.up ⁻¹' s)
ULift.up_sInf 📋 Mathlib.Order.CompleteLattice.Lemmas
{α : Type u_1} [InfSet α] (s : Set α) : { down := sInf s } = sInf (ULift.down ⁻¹' s)
ULift.up_sSup 📋 Mathlib.Order.CompleteLattice.Lemmas
{α : Type u_1} [SupSet α] (s : Set α) : { down := sSup s } = sSup (ULift.down ⁻¹' s)
ULift.down_iInf 📋 Mathlib.Order.CompleteLattice.Lemmas
{α : Type u_1} {ι : Sort u_4} [InfSet α] (f : ι → ULift.{v, u_1} α) : (⨅ i, f i).down = ⨅ i, (f i).down
ULift.down_iSup 📋 Mathlib.Order.CompleteLattice.Lemmas
{α : Type u_1} {ι : Sort u_4} [SupSet α] (f : ι → ULift.{v, u_1} α) : (⨆ i, f i).down = ⨆ i, (f i).down
ULift.up_iInf 📋 Mathlib.Order.CompleteLattice.Lemmas
{α : Type u_1} {ι : Sort u_4} [InfSet α] (f : ι → α) : { down := ⨅ i, f i } = ⨅ i, { down := f i }
ULift.up_iSup 📋 Mathlib.Order.CompleteLattice.Lemmas
{α : Type u_1} {ι : Sort u_4} [SupSet α] (f : ι → α) : { down := ⨆ i, f i } = ⨆ i, { down := f i }
List.findM?' 📋 Mathlib.Data.List.Defs
{m : Type u → Type v} [Monad m] {α : Type u} (p : α → m (ULift.{u, 0} Bool)) : List α → m (Option α)
instFiniteULift 📋 Mathlib.Data.Finite.Defs
{α : Type v} [Finite α] : Finite (ULift.{u, v} α)
instInfiniteULift 📋 Mathlib.Data.Finite.Defs
{α : Type v} [Infinite α] : Infinite (ULift.{u, v} α)
ULift.fintype 📋 Mathlib.Data.Fintype.Basic
(α : Type u_4) [Fintype α] : Fintype (ULift.{u_5, u_4} α)
Fintype.card_ulift 📋 Mathlib.Data.Fintype.Card
(α : Type u_4) [Fintype α] : Fintype.card (ULift.{u_5, u_4} α) = Fintype.card α
ULift.add 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Add α] : Add (ULift.{u_2, u} α)
ULift.addCancelCommMonoid 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [AddCancelCommMonoid α] : AddCancelCommMonoid (ULift.{u_2, u} α)
ULift.addCancelMonoid 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [AddCancelMonoid α] : AddCancelMonoid (ULift.{u_2, u} α)
ULift.addCommGroup 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [AddCommGroup α] : AddCommGroup (ULift.{u_2, u} α)
ULift.addCommGroupWithOne 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [AddCommGroupWithOne α] : AddCommGroupWithOne (ULift.{u_2, u} α)
ULift.addCommMonoid 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [AddCommMonoid α] : AddCommMonoid (ULift.{u_2, u} α)
ULift.addCommMonoidWithOne 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [AddCommMonoidWithOne α] : AddCommMonoidWithOne (ULift.{u_2, u} α)
ULift.addCommSemigroup 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [AddCommSemigroup α] : AddCommSemigroup (ULift.{u_2, u} α)
ULift.addGroup 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [AddGroup α] : AddGroup (ULift.{u_2, u} α)
ULift.addGroupWithOne 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [AddGroupWithOne α] : AddGroupWithOne (ULift.{u_2, u} α)
ULift.addLeftCancelMonoid 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [AddLeftCancelMonoid α] : AddLeftCancelMonoid (ULift.{u_2, u} α)
ULift.addLeftCancelSemigroup 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [AddLeftCancelSemigroup α] : AddLeftCancelSemigroup (ULift.{u_2, u} α)
ULift.addMonoid 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [AddMonoid α] : AddMonoid (ULift.{u_2, u} α)
ULift.addMonoidWithOne 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [AddMonoidWithOne α] : AddMonoidWithOne (ULift.{u_2, u} α)
ULift.addRightCancelMonoid 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [AddRightCancelMonoid α] : AddRightCancelMonoid (ULift.{u_2, u} α)
ULift.addRightCancelSemigroup 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [AddRightCancelSemigroup α] : AddRightCancelSemigroup (ULift.{u_2, u} α)
ULift.addSemigroup 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [AddSemigroup α] : AddSemigroup (ULift.{u_2, u} α)
ULift.addZeroClass 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [AddZeroClass α] : AddZeroClass (ULift.{u_2, u} α)
ULift.cancelCommMonoid 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [CancelCommMonoid α] : CancelCommMonoid (ULift.{u_2, u} α)
ULift.cancelMonoid 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [CancelMonoid α] : CancelMonoid (ULift.{u_2, u} α)
ULift.commGroup 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [CommGroup α] : CommGroup (ULift.{u_2, u} α)
ULift.commMonoid 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [CommMonoid α] : CommMonoid (ULift.{u_2, u} α)
ULift.commSemigroup 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [CommSemigroup α] : CommSemigroup (ULift.{u_2, u} α)
ULift.div 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Div α] : Div (ULift.{u_2, u} α)
ULift.divInvMonoid 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [DivInvMonoid α] : DivInvMonoid (ULift.{u_2, u} α)
ULift.group 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Group α] : Group (ULift.{u_2, u} α)
ULift.instIntCast 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [IntCast α] : IntCast (ULift.{u_2, u} α)
ULift.instNatCast 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [NatCast α] : NatCast (ULift.{u_2, u} α)
ULift.inv 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Inv α] : Inv (ULift.{u_2, u} α)
ULift.leftCancelMonoid 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [LeftCancelMonoid α] : LeftCancelMonoid (ULift.{u_2, u} α)
ULift.leftCancelSemigroup 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [LeftCancelSemigroup α] : LeftCancelSemigroup (ULift.{u_2, u} α)
ULift.monoid 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Monoid α] : Monoid (ULift.{u_2, u} α)
ULift.mul 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Mul α] : Mul (ULift.{u_2, u} α)
ULift.mulOneClass 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [MulOneClass α] : MulOneClass (ULift.{u_2, u} α)
ULift.neg 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Neg α] : Neg (ULift.{u_2, u} α)
ULift.nontrivial 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Nontrivial α] : Nontrivial (ULift.{u_2, u} α)
ULift.one 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [One α] : One (ULift.{u_2, u} α)
ULift.rightCancelMonoid 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [RightCancelMonoid α] : RightCancelMonoid (ULift.{u_2, u} α)
ULift.rightCancelSemigroup 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [RightCancelSemigroup α] : RightCancelSemigroup (ULift.{u_2, u} α)
ULift.semigroup 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Semigroup α] : Semigroup (ULift.{u_2, u} α)
ULift.sub 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Sub α] : Sub (ULift.{u_2, u} α)
ULift.subNegAddMonoid 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [SubNegMonoid α] : SubNegMonoid (ULift.{u_2, u} α)
ULift.zero 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Zero α] : Zero (ULift.{u_2, u} α)
ULift.pow 📋 Mathlib.Algebra.Group.ULift
{α : Type u} {β : Type u_1} [Pow α β] : Pow (ULift.{u_2, u} α) β
ULift.smul 📋 Mathlib.Algebra.Group.ULift
{α : Type u} {β : Type u_1} [SMul α β] : SMul α (ULift.{u_2, u_1} β)
ULift.vadd 📋 Mathlib.Algebra.Group.ULift
{α : Type u} {β : Type u_1} [VAdd α β] : VAdd α (ULift.{u_2, u_1} β)
AddEquiv.ulift 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Add α] : ULift.{u_2, u} α ≃+ α
MulEquiv.ulift 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Mul α] : ULift.{u_2, u} α ≃* α
ULift.down_intCast 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [IntCast α] (n : ℤ) : (↑n).down = ↑n
ULift.down_natCast 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [NatCast α] (n : ℕ) : (↑n).down = ↑n
ULift.up_intCast 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [IntCast α] (n : ℤ) : { down := ↑n } = ↑n
ULift.up_natCast 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [NatCast α] (n : ℕ) : { down := ↑n } = ↑n
ULift.one.eq_1 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [One α] : ULift.one = { one := { down := 1 } }
ULift.zero.eq_1 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Zero α] : ULift.zero = { zero := { down := 0 } }
ULift.inv_down 📋 Mathlib.Algebra.Group.ULift
{α : Type u} {x : ULift.{v, u} α} [Inv α] : x⁻¹.down = x.down⁻¹
ULift.neg_down 📋 Mathlib.Algebra.Group.ULift
{α : Type u} {x : ULift.{v, u} α} [Neg α] : (-x).down = -x.down
ULift.one_down 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [One α] : ULift.down 1 = 1
ULift.zero_down 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Zero α] : ULift.down 0 = 0
ULift.inv.eq_1 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Inv α] : ULift.inv = { inv := fun f => { down := f.down⁻¹ } }
ULift.neg.eq_1 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Neg α] : ULift.neg = { neg := fun f => { down := -f.down } }
AddEquiv.ulift.eq_1 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Add α] : AddEquiv.ulift = { toEquiv := Equiv.ulift, map_add' := ⋯ }
MulEquiv.ulift.eq_1 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Mul α] : MulEquiv.ulift = { toEquiv := Equiv.ulift, map_mul' := ⋯ }
ULift.down_ofNat 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [NatCast α] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).down = OfNat.ofNat n
ULift.up_ofNat 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [NatCast α] (n : ℕ) [n.AtLeastTwo] : { down := OfNat.ofNat n } = OfNat.ofNat n
ULift.add.eq_1 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Add α] : ULift.add = { add := fun f g => { down := f.down + g.down } }
ULift.div.eq_1 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Div α] : ULift.div = { div := fun f g => { down := f.down / g.down } }
ULift.mul.eq_1 📋 Mathlib.Algebra.Group.ULift
{α : Type u} [Mul α] : ULift.mul = { mul := fun f g => { down := f.down * g.down } }

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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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 19971e9 serving mathlib revision bce1d65