Loogle!

Result

Found 75 declarations mentioning flip.

• flip 📋 Init.Core
  {α : Sort u} {β : Sort v} {φ : Sort w} (f : α → β → φ) : β → α → φ
• flip_flip 📋 Init.Core
  {α : Sort u} {β : Sort v} {φ : Sort w} {f : α → β → φ} : flip (flip f) = f
• List.Pairwise.forall_of_forall_of_flip 📋 Init.Data.List.Pairwise
  {α✝ : Type u_1} {l : List α✝} {R : α✝ → α✝ → Prop} (h₁ : ∀ x ∈ l, R x x) (h₂ : List.Pairwise R l) (h₃ : List.Pairwise (flip R) l) ⦃x : α✝⦄ : x ∈ l → ∀ ⦃y : α✝⦄, y ∈ l → R x y
• Std.Internal.instLawfulMonadLiftBindFunctionFlipForallBindOfLawfulMonad 📋 Init.Data.Iterators.Internal.LawfulMonadLiftFunction
  {m : Type u → Type v} [Monad m] [LawfulMonad m] : Std.Internal.LawfulMonadLiftBindFunction fun x x_1 => flip bind
• List.scanl_eq_scanr_reverse 📋 Init.Data.List.Scan.Lemmas
  {β : Type u_1} {α : Type u_2} {init : β} {as : List α} {f : β → α → β} : List.scanl f init as = (List.scanr (flip f) init as.reverse).reverse
• List.scanl_reverse 📋 Init.Data.List.Scan.Lemmas
  {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : List α} : List.scanl f init as.reverse = (List.scanr (flip f) init as).reverse
• List.scanr_eq_scanl_reverse 📋 Init.Data.List.Scan.Lemmas
  {α : Type u_1} {β : Type u_2} {init : β} {as : List α} {f : α → β → β} : List.scanr f init as = (List.scanl (flip f) init as.reverse).reverse
• List.scanr_reverse 📋 Init.Data.List.Scan.Lemmas
  {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : List α} : List.scanr f init as.reverse = (List.scanl (flip f) init as).reverse
• List.scanlM_eq_scanrM_reverse 📋 Init.Data.List.Scan.Lemmas
  {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} {as : List α} [Monad m] {f : β → α → m β} : List.scanlM f init as = List.reverse <$> List.scanrM (flip f) init as.reverse
• List.scanlM_reverse 📋 Init.Data.List.Scan.Lemmas
  {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} {as : List α} [Monad m] {f : β → α → m β} : List.scanlM f init as.reverse = List.reverse <$> List.scanrM (flip f) init as
• List.scanrM_eq_scanlM_reverse 📋 Init.Data.List.Scan.Lemmas
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} {as : List α} [Monad m] [LawfulMonad m] {f : α → β → m β} : List.scanrM f init as = List.reverse <$> List.scanlM (flip f) init as.reverse
• List.scanrM_reverse 📋 Init.Data.List.Scan.Lemmas
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} {as : List α} [Monad m] [LawfulMonad m] {f : α → β → m β} : List.scanrM f init as.reverse = List.reverse <$> List.scanlM (flip f) init as
• Std.instOrientedCmpFlipOrdering_batteries 📋 Batteries.Classes.Order
  {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} [inst : Std.OrientedCmp cmp] : Std.OrientedCmp (flip cmp)
• Std.instTransCmpFlipOrdering_batteries 📋 Batteries.Classes.Order
  {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} [inst : Std.TransCmp cmp] : Std.TransCmp (flip cmp)
• Batteries.instOrientedCmpFlipOrdering 📋 Batteries.Classes.Deprecated
  {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} [inst : Batteries.OrientedCmp cmp] : Batteries.OrientedCmp (flip cmp)
• Batteries.instTransCmpFlipOrdering 📋 Batteries.Classes.Deprecated
  {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} [inst : Batteries.TransCmp cmp] : Batteries.TransCmp (flip cmp)
• Array.scanl_reverse 📋 Batteries.Data.Array.Scan
  {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : Array α} : Array.scanl f init as.reverse = (Array.scanr (flip f) init as).reverse
• Array.scanlM_reverse 📋 Batteries.Data.Array.Scan
  {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} [Monad m] [LawfulMonad m] {f : β → α → m β} {as : Array α} : Array.scanlM f init as.reverse = Array.reverse <$> Array.scanrM (flip f) init as
• Batteries.RBNode.Ordered.reverse 📋 Batteries.Data.RBMap.WF
  {α : Type u_1} {cmp : α → α → Ordering} {t : Batteries.RBNode α} : Batteries.RBNode.Ordered cmp t → Batteries.RBNode.Ordered (flip cmp) t.reverse
• Batteries.RBNode.cmpLT.flip 📋 Batteries.Data.RBMap.WF
  {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {x y : α✝} (h₁ : Batteries.RBNode.cmpLT cmp x y) : Batteries.RBNode.cmpLT (flip cmp) y x
• Batteries.RBNode.reverse_ins 📋 Batteries.Data.RBMap.WF
  {α : Type u_1} {cmp : α → α → Ordering} {x : α} [inst : Std.OrientedCmp cmp] {t : Batteries.RBNode α} : (Batteries.RBNode.ins cmp x t).reverse = Batteries.RBNode.ins (flip cmp) x t.reverse
• Batteries.RBNode.reverse_insert 📋 Batteries.Data.RBMap.WF
  {α : Type u_1} {cmp : α → α → Ordering} {x : α} [inst : Std.OrientedCmp cmp] {t : Batteries.RBNode α} : (Batteries.RBNode.insert cmp t x).reverse = Batteries.RBNode.insert (flip cmp) t.reverse x
• Batteries.RBNode.instIsCutFlipOrderingSwap 📋 Batteries.Data.RBMap.Lemmas
  {α : Type u_1} (cmp : α → α → Ordering) (cut : α → Ordering) [Batteries.RBNode.IsCut cmp cut] : Batteries.RBNode.IsCut (flip cmp) fun x => (cut x).swap
• Batteries.RBNode.instIsStrictCutFlipOrderingSwap 📋 Batteries.Data.RBMap.Lemmas
  {α : Type u_1} (cmp : α → α → Ordering) (cut : α → Ordering) [Batteries.RBNode.IsStrictCut cmp cut] : Batteries.RBNode.IsStrictCut (flip cmp) fun x => (cut x).swap
• Batteries.RBNode.Mem_reverse 📋 Batteries.Data.RBMap.Lemmas
  {α : Type u_1} {cmp : α → α → Ordering} {x : α} [Std.OrientedCmp cmp] {t : Batteries.RBNode α} : Batteries.RBNode.Mem cmp x t.reverse ↔ Batteries.RBNode.Mem (flip cmp) x t
• Batteries.RBNode.foldl_reverse 📋 Batteries.Data.RBMap.Lemmas
  {α : Type u_1} {β : Type u_2} {t : Batteries.RBNode α} {f : β → α → β} {init : β} : Batteries.RBNode.foldl f init t.reverse = Batteries.RBNode.foldr (flip f) t init
• Batteries.RBNode.foldr_reverse 📋 Batteries.Data.RBMap.Lemmas
  {α : Type u_1} {β : Type u_2} {t : Batteries.RBNode α} {f : α → β → β} {init : β} : Batteries.RBNode.foldr f t.reverse init = Batteries.RBNode.foldl (flip f) init t
• Function.flip_def 📋 Mathlib.Logic.Function.Defs
  {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {f : α → β → φ} : flip f = fun b a => f a b
• Function.flip_curry 📋 Mathlib.Logic.Function.Basic
  {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α × β → γ) : flip (Function.curry f) = Function.curry (f ∘ Prod.swap)
• Function.uncurry_flip 📋 Mathlib.Logic.Function.Basic
  {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → β → γ) : Function.uncurry (flip f) = Function.uncurry f ∘ Prod.swap
• Relator.LeftUnique.flip 📋 Mathlib.Logic.Relator
  {α : Type u_1} {β : Type u_2} {r : α → β → Prop} (h : Relator.LeftUnique r) : Relator.RightUnique (flip r)
• Symmetric.flip_eq 📋 Mathlib.Logic.Relation
  {α : Sort u_1} {r : α → α → Prop} (h : Symmetric r) : flip r = r
• flip_eq_iff 📋 Mathlib.Logic.Relation
  {α : Sort u_1} {r : α → α → Prop} : flip r = r ↔ Symmetric r
• Relation.flip_comp 📋 Mathlib.Logic.Relation
  {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {r : α → β → Prop} {p : β → γ → Prop} : flip (Relation.Comp r p) = Relation.Comp (flip p) (flip r)
• Contravariant.flip 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} (h : Contravariant M N μ r) : Contravariant M N μ (flip r)
• Covariant.flip 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} (h : Covariant M N μ r) : Covariant M N μ (flip r)
• contravariant_flip_iff 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (N : Type u_2) (r : N → N → Prop) (mu : N → N → N) [h : Std.Commutative mu] : Contravariant N N (flip mu) r ↔ Contravariant N N mu r
• covariant_flip_iff 📋 Mathlib.Algebra.Order.Monoid.Unbundled.Defs
  (N : Type u_2) (r : N → N → Prop) (mu : N → N → N) [h : Std.Commutative mu] : Covariant N N (flip mu) r ↔ Covariant N N mu r
• IsSymmOp.flip_eq 📋 Mathlib.Logic.OpClass
  {α : Sort u} {β : Sort v} (op : α → α → β) [IsSymmOp op] : flip op = op
• CommApplicative.commutative_map 📋 Mathlib.Control.Basic
  {m : Type u → Type v} [h : Applicative m] [CommApplicative m] {α β γ : Type u} (a : m α) (b : m β) {f : α → β → γ} : f <$> a <*> b = flip f <$> b <*> a
• List.Forall₂.flip 📋 Mathlib.Data.List.Forall2
  {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : List α} {b : List β} : List.Forall₂ (flip R) b a → List.Forall₂ R a b
• IsChain.symm 📋 Mathlib.Order.Preorder.Chain
  {α : Type u_1} {r : α → α → Prop} {s : Set α} (h : IsChain r s) : IsChain (flip r) s
• IsMaxChain.symm 📋 Mathlib.Order.Preorder.Chain
  {α : Type u_1} {r : α → α → Prop} {s : Set α} (h : IsMaxChain r s) : IsMaxChain (flip r) s
• IsAntichain.flip 📋 Mathlib.Order.Antichain
  {α : Type u_1} {r : α → α → Prop} {s : Set α} (hs : IsAntichain r s) : IsAntichain (flip r) s
• IsMaxAntichain.symm 📋 Mathlib.Order.Antichain
  {α : Type u_1} {r : α → α → Prop} {s : Set α} (h : IsMaxAntichain r s) : IsMaxAntichain (flip r) s
• IsStrongAntichain.flip 📋 Mathlib.Order.Antichain
  {α : Type u_1} {r : α → α → Prop} {s : Set α} [Std.Symm r] (hs : IsStrongAntichain r s) : IsStrongAntichain (flip r) s
• Multiset.rel_flip 📋 Mathlib.Data.Multiset.ZeroCons
  {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset β} {t : Multiset α} : Multiset.Rel (flip r) s t ↔ Multiset.Rel r t s
• Acc.list_chain' 📋 Mathlib.Data.List.Chain
  {α : Type u_1} {r : α → α → Prop} {l : List.chains r} (acc : ∀ a ∈ (↑l).head?, Acc r a) : Acc (List.lex_chains r) l
• List.Vector.instTraversableFlipNat 📋 Mathlib.Data.Vector.Basic
  {n : ℕ} : Traversable (flip List.Vector n)
• List.Vector.instLawfulTraversableFlipNat 📋 Mathlib.Data.Vector.Basic
  {n : ℕ} : LawfulTraversable (flip List.Vector n)
• Filter.IsBounded.isCobounded_flip 📋 Mathlib.Order.Filter.IsBounded
  {α : Type u_1} {r : α → α → Prop} {f : Filter α} [IsTrans α r] [f.NeBot] : Filter.IsBounded r f → Filter.IsCobounded (flip r) f
• Filter.IsBoundedUnder.isCoboundedUnder_flip 📋 Mathlib.Order.Filter.IsBounded
  {α : Type u_1} {γ : Type u_3} {r : α → α → Prop} {u : γ → α} {l : Filter γ} [IsTrans α r] [l.NeBot] (h : Filter.IsBoundedUnder r l u) : Filter.IsCoboundedUnder (flip r) l u
• span_flip_eq_top_iff_linearIndependent 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {ι : Type u_1} {α : Type u_2} {F : Type u_3} [Finite ι] [Field F] {f : ι → α → F} : Submodule.span F (Set.range (flip f)) = ⊤ ↔ LinearIndependent F f
• Bifunctor.flip 📋 Mathlib.Control.Bifunctor
  {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] : Bifunctor (flip F)
• LawfulBifunctor.flip 📋 Mathlib.Control.Bifunctor
  {F : Type u₀ → Type u₁ → Type u₂} [Bifunctor F] [LawfulBifunctor F] : LawfulBifunctor (flip F)
• Matrix.vec_of 📋 Mathlib.LinearAlgebra.Matrix.Vec
  {m : Type u_2} {n : Type u_1} {R : Type u_3} (f : m → n → R) : (Matrix.of f).vec = Function.uncurry (flip f)
• StateTransition.EvalsTo.mk 📋 Mathlib.Computability.StateTransition
  {σ : Type u_1} {f : σ → Option σ} {a : σ} {b : Option σ} (steps : ℕ) (evals_in_steps : (flip bind f)^[steps] (some a) = b) : StateTransition.EvalsTo f a b
• StateTransition.EvalsTo.evals_in_steps 📋 Mathlib.Computability.StateTransition
  {σ : Type u_1} {f : σ → Option σ} {a : σ} {b : Option σ} (self : StateTransition.EvalsTo f a b) : (flip bind f)^[self.steps] (some a) = b
• Bitraversable.flip 📋 Mathlib.Control.Bitraversable.Instances
  {t : Type u → Type u → Type u} [Bitraversable t] : Bitraversable (flip t)
• LawfulBitraversable.flip 📋 Mathlib.Control.Bitraversable.Instances
  {t : Type u → Type u → Type u} [Bitraversable t] [LawfulBitraversable t] : LawfulBitraversable (flip t)
• flip.bitraverse 📋 Mathlib.Control.Bitraversable.Instances
  {t : Type u → Type u → Type u} [Bitraversable t] {F : Type u → Type u} [Applicative F] {α α' β β' : Type u} (f : α → F α') (f' : β → F β') : flip t α β → F (flip t α' β')
• Monoid.Foldr.ofFreeMonoid_apply 📋 Mathlib.Control.Fold
  {α β : Type u} (f : α → β → β) (xs : FreeMonoid α) (a✝ : β) : (Monoid.Foldr.ofFreeMonoid f) xs a✝ = flip (List.foldr f) (FreeMonoid.toList xs) a✝
• Traversable.foldl.ofFreeMonoid_comp_of 📋 Mathlib.Control.Fold
  {α β : Type u} (f : α → β → α) : ⇑(Monoid.Foldl.ofFreeMonoid f) ∘ FreeMonoid.of = Monoid.Foldl.mk ∘ flip f
• Monoid.Foldl.ofFreeMonoid_apply 📋 Mathlib.Control.Fold
  {α β : Type u} (f : β → α → β) (xs : FreeMonoid α) : (Monoid.Foldl.ofFreeMonoid f) xs = MulOpposite.op (flip (List.foldl f) (FreeMonoid.toList xs))
• Monoid.foldrM.ofFreeMonoid_apply 📋 Mathlib.Control.Fold
  {m : Type u → Type u} [Monad m] {α β : Type u} [LawfulMonad m] (f : α → β → m β) (xs : FreeMonoid α) (a✝ : CategoryTheory.KleisliCat.mk m β) : (Monoid.foldrM.ofFreeMonoid f) xs a✝ = flip (List.foldrM f) (FreeMonoid.toList xs) a✝
• Traversable.foldlm.ofFreeMonoid_comp_of 📋 Mathlib.Control.Fold
  {α β : Type u} {m : Type u → Type u} [Monad m] [LawfulMonad m] (f : α → β → m α) : ⇑(Monoid.foldlM.ofFreeMonoid f) ∘ FreeMonoid.of = Monoid.foldlM.mk ∘ flip f
• Monoid.foldlM.ofFreeMonoid_apply 📋 Mathlib.Control.Fold
  {m : Type u → Type u} [Monad m] {α β : Type u} [LawfulMonad m] (f : β → α → m β) (xs : FreeMonoid α) : (Monoid.foldlM.ofFreeMonoid f) xs = MulOpposite.op (flip (List.foldlM f) (FreeMonoid.toList xs))
• List.foldl_cons_nil 📋 Mathlib.Data.List.Fold
  {α : Type u_1} {l : List α} : List.foldl (flip List.cons) [] l = l.reverse
• List.foldl_eq_foldr' 📋 Mathlib.Data.List.Fold
  {α : Type u_1} {β : Type u_2} {l : List α} {v : β → α → β} {b : β} [RightCommutative v] : List.foldr (flip v) b l = List.foldl v b l
• List.foldl_flip_eq_foldr 📋 Mathlib.Data.List.Fold
  {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β → β} {b : β} [LeftCommutative f] : List.foldl (flip f) b l = List.foldr f b l
• List.foldr_flip_eq_foldl 📋 Mathlib.Data.List.Fold
  {α : Type u_1} {β : Type u_2} {l : List α} {v : β → α → β} {b : β} [RightCommutative v] : List.foldr (flip v) b l = List.foldl v b l
• List.zipWith_flip 📋 Mathlib.Data.List.Map2
  {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (as : List α) (bs : List β) : List.zipWith (flip f) bs as = List.zipWith f as bs
• List.Vector.map₂_flip 📋 Mathlib.Data.Vector.MapLemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (xs : List.Vector α n) (ys : List.Vector β n) (f : α → β → γ) : List.Vector.map₂ f xs ys = List.Vector.map₂ (flip f) ys xs
• List.Vector.mapAccumr₂_flip 📋 Mathlib.Data.Vector.MapLemmas
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : ℕ} {s : σ} (xs : List.Vector α n) (ys : List.Vector β n) (f : α → β → σ → σ × γ) : List.Vector.mapAccumr₂ f xs ys s = List.Vector.mapAccumr₂ (flip f) ys xs s
• Set.chainHeight_flip 📋 Mathlib.Order.Height
  {α : Type u_1} (s : Set α) (r : α → α → Prop) : s.chainHeight (flip r) = s.chainHeight r

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.

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 8e80836 serving mathlib revision 6ef8cc2