Loogle!

Result

Found 215 declarations mentioning Prod.fst, LT.lt, and Prod.snd. Of these, 24 match your pattern(s).

• Finset.offDiag_filter_lt_eq_filter_le 📋 Mathlib.Data.Finset.Prod
  {ι : Type u_4} [PartialOrder ι] [DecidableLE ι] [DecidableLT ι] (s : Finset ι) : {i ∈ s.offDiag | i.1 < i.2} = {i ∈ s.offDiag | i.1 ≤ i.2}
• isOpen_lt_prod 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] : IsOpen {p | p.1 < p.2}
• Finset.sum_sym2_filter_not_isDiag 📋 Mathlib.Algebra.BigOperators.Sym
  {ι : Type u_1} {M : Type u_2} [LinearOrder ι] [AddCommMonoid M] (s : Finset ι) (p : Sym2 ι → M) : ∑ i ∈ s.sym2 with ¬i.IsDiag, p i = ∑ i ∈ s.offDiag with i.1 < i.2, p s(i.1, i.2)
• CategoryTheory.Limits.MultispanShape.ofLinearOrder_L 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  (ι : Type w) [LinearOrder ι] : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).L = ↑{x | x.1 < x.2}
• CategoryTheory.Limits.MultispanIndex.toLinearOrder_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type w} (I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C) [LinearOrder ι] (j : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).L) : I.toLinearOrder.left j = I.left ↑j
• CategoryTheory.Limits.MultispanShape.ofLinearOrder_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  (ι : Type w) [LinearOrder ι] (x : ↑{x | x.1 < x.2}) : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).fst x = (↑x).1
• CategoryTheory.Limits.MultispanShape.ofLinearOrder_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  (ι : Type w) [LinearOrder ι] (x : ↑{x | x.1 < x.2}) : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).snd x = (↑x).2
• CategoryTheory.Limits.WalkingMultispan.inclusionOfLinearOrder_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  (ι : Type w) [LinearOrder ι] (x : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι)) : (CategoryTheory.Limits.WalkingMultispan.inclusionOfLinearOrder ι).obj x = match x with | CategoryTheory.Limits.WalkingMultispan.left a => CategoryTheory.Limits.WalkingMultispan.left ↑a | CategoryTheory.Limits.WalkingMultispan.right b => CategoryTheory.Limits.WalkingMultispan.right b
• CategoryTheory.Limits.MultispanIndex.toLinearOrder_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type w} (I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C) [LinearOrder ι] (j : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).L) : I.toLinearOrder.fst j = I.fst ↑j
• CategoryTheory.Limits.MultispanIndex.toLinearOrder_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type w} (I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C) [LinearOrder ι] (j : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).L) : I.toLinearOrder.snd j = I.snd ↑j
• CategoryTheory.Limits.MultispanIndex.toLinearOrderMultispanIso_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type w} (I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C) [LinearOrder ι] (X : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι)) : I.toLinearOrderMultispanIso.hom.app X = (match X with | CategoryTheory.Limits.WalkingMultispan.left a => CategoryTheory.Iso.refl (I.left ↑a) | CategoryTheory.Limits.WalkingMultispan.right a => CategoryTheory.Iso.refl (I.right a)).hom
• CategoryTheory.Limits.MultispanIndex.toLinearOrderMultispanIso_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type w} (I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C) [LinearOrder ι] (X : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι)) : I.toLinearOrderMultispanIso.inv.app X = (match X with | CategoryTheory.Limits.WalkingMultispan.left a => CategoryTheory.Iso.refl (I.left ↑a) | CategoryTheory.Limits.WalkingMultispan.right a => CategoryTheory.Iso.refl (I.right a)).inv
• CategoryTheory.Limits.WalkingMultispan.inclusionOfLinearOrder_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  (ι : Type w) [LinearOrder ι] {x y : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι)} (f : x ⟶ y) : (CategoryTheory.Limits.WalkingMultispan.inclusionOfLinearOrder ι).map f = match x, y, f with | x, .(x), CategoryTheory.Limits.WalkingMultispan.Hom.id .(x) => CategoryTheory.CategoryStruct.id (match x with | CategoryTheory.Limits.WalkingMultispan.left a => CategoryTheory.Limits.WalkingMultispan.left ↑a | CategoryTheory.Limits.WalkingMultispan.right b => CategoryTheory.Limits.WalkingMultispan.right b) | .(CategoryTheory.Limits.WalkingMultispan.left b), .(CategoryTheory.Limits.WalkingMultispan.right ((CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).fst b)), CategoryTheory.Limits.WalkingMultispan.Hom.fst b => CategoryTheory.Limits.WalkingMultispan.Hom.fst ↑b | .(CategoryTheory.Limits.WalkingMultispan.left b), .(CategoryTheory.Limits.WalkingMultispan.right ((CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).snd b)), CategoryTheory.Limits.WalkingMultispan.Hom.snd b => CategoryTheory.Limits.WalkingMultispan.Hom.snd ↑b
• LTSeries.map_length 📋 Mathlib.Order.RelSeries
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (p : LTSeries α) (f : α → β) (hf : StrictMono f) : (p.map f hf).length = p.length
• LTSeries.comap_length 📋 Mathlib.Order.RelSeries
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (p : LTSeries β) (f : α → β) (comap : ∀ ⦃x y : α⦄, f x < f y → x < y) (surjective : Function.Surjective f) : (p.comap f comap surjective).length = p.length
• LTSeries.map_toFun 📋 Mathlib.Order.RelSeries
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (p : LTSeries α) (f : α → β) (hf : StrictMono f) (a✝ : Fin (p.length + 1)) : (p.map f hf).toFun a✝ = f (p.toFun a✝)
• LTSeries.comap_toFun 📋 Mathlib.Order.RelSeries
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (p : LTSeries β) (f : α → β) (comap : ∀ ⦃x y : α⦄, f x < f y → x < y) (surjective : Function.Surjective f) (i : Fin (p.length + 1)) : (p.comap f comap surjective).toFun i = ⋯.choose
• measurable_lt 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [LinearOrder α] [SecondCountableTopology α] [OrderClosedTopology α] : Measurable fun p => p.1 < p.2
• measurableSet_lt' 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [LinearOrder α] [SecondCountableTopology α] [OrderClosedTopology α] : MeasurableSet {p | p.1 < p.2}
• nullMeasurableSet_lt' 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [LinearOrder α] [SecondCountableTopology α] [OrderClosedTopology α] {μ : MeasureTheory.Measure (α × α)} : MeasureTheory.NullMeasurableSet {p | p.1 < p.2} μ
• Affine.Simplex.Scalene.eq_1 📋 Mathlib.Analysis.Normed.Affine.Simplex
  {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [SeminormedAddCommGroup V] [PseudoMetricSpace P] [Module R V] [NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex R P n) : s.Scalene = Function.Injective fun i => dist (s.points (↑i).1) (s.points (↑i).2)
• NNReal.agmSequences_fst_lt_snd_of_ne 📋 Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
  {x y : NNReal} (h : x ≠ y) (n m : ℕ) : (x.agmSequences y n).1 < (x.agmSequences y m).2
• AbsolutelyContinuousOnInterval.dist_le_of_pairwiseDisjoint_hasSum 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
  {X : Type u_1} [PseudoMetricSpace X] {f : ℝ → X} {d b y : ℝ} (hdb : d ≤ b) (hf : AbsolutelyContinuousOnInterval f d b) {u : Set (ℝ × ℝ)} (hu₁ : ∀ z ∈ u, d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) (hu₂ : u.PairwiseDisjoint fun z => Set.Icc z.1 z.2) (hu₃ : HasSum (fun z => (↑z).2 - (↑z).1) (b - d)) (hu₄ : HasSum (fun z => dist (f (↑z).1) (f (↑z).2)) y) : dist (f d) (f b) ≤ y
• exists_dist_slope_lt_pairwiseDisjoint_hasSum 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
  {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f f' : ℝ → F} {d b η : ℝ} (hdb : d ≤ b) (hf : ∀ᵐ (x : ℝ), x ∈ Set.Ioo d b → HasDerivAt f (f' x) x) (hη : 0 < η) : ∃ u, (∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η) ∧ (u.PairwiseDisjoint fun z => Set.Icc z.1 z.2) ∧ HasSum (fun z => (↑z).2 - (↑z).1) (b - d)

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 36960b0 serving mathlib revision cbbc48f