Loogle!

Result

Found 50 declarations mentioning MeasureTheory.SimpleFunc.map.

• MeasureTheory.SimpleFunc.map 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (g : β → γ) (f : MeasureTheory.SimpleFunc α β) : MeasureTheory.SimpleFunc α γ
• MeasureTheory.SimpleFunc.map_const 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (g : β → γ) (b : β) : MeasureTheory.SimpleFunc.map g (MeasureTheory.SimpleFunc.const α b) = MeasureTheory.SimpleFunc.const α (g b)
• MeasureTheory.SimpleFunc.eapproxDiff.eq_1 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} [MeasurableSpace α] (f : α → ENNReal) : MeasureTheory.SimpleFunc.eapproxDiff f 0 = MeasureTheory.SimpleFunc.map ENNReal.toNNReal (MeasureTheory.SimpleFunc.eapprox f 0)
• MeasureTheory.SimpleFunc.instInv.eq_1 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Inv β] : MeasureTheory.SimpleFunc.instInv = { inv := fun f => MeasureTheory.SimpleFunc.map Inv.inv f }
• MeasureTheory.SimpleFunc.instNeg.eq_1 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Neg β] : MeasureTheory.SimpleFunc.instNeg = { neg := fun f => MeasureTheory.SimpleFunc.map Neg.neg f }
• MeasureTheory.SimpleFunc.map_fst_pair 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α γ) : MeasureTheory.SimpleFunc.map Prod.fst (f.pair g) = f
• MeasureTheory.SimpleFunc.map_snd_pair 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (g : MeasureTheory.SimpleFunc α γ) : MeasureTheory.SimpleFunc.map Prod.snd (f.pair g) = g
• MeasureTheory.SimpleFunc.range_map 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [DecidableEq γ] (g : β → γ) (f : MeasureTheory.SimpleFunc α β) : (MeasureTheory.SimpleFunc.map g f).range = Finset.image g f.range
• MeasureTheory.SimpleFunc.map_coe_ennreal_restrict 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α NNReal) (s : Set α) : MeasureTheory.SimpleFunc.map ENNReal.ofNNReal (f.restrict s) = (MeasureTheory.SimpleFunc.map ENNReal.ofNNReal f).restrict s
• MeasureTheory.SimpleFunc.map_coe_nnreal_restrict 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α NNReal) (s : Set α) : MeasureTheory.SimpleFunc.map NNReal.toReal (f.restrict s) = (MeasureTheory.SimpleFunc.map NNReal.toReal f).restrict s
• MeasureTheory.SimpleFunc.map_map 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace α] (g : β → γ) (h : γ → δ) (f : MeasureTheory.SimpleFunc α β) : MeasureTheory.SimpleFunc.map h (MeasureTheory.SimpleFunc.map g f) = MeasureTheory.SimpleFunc.map (h ∘ g) f
• MeasureTheory.SimpleFunc.hasNatPow.eq_1 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Monoid β] : MeasureTheory.SimpleFunc.hasNatPow = { pow := fun f n => MeasureTheory.SimpleFunc.map (fun x => x ^ n) f }
• MeasureTheory.SimpleFunc.map_apply 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (g : β → γ) (f : MeasureTheory.SimpleFunc α β) (a : α) : (MeasureTheory.SimpleFunc.map g f) a = g (f a)
• MeasureTheory.SimpleFunc.instSMul.eq_1 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [SMul K β] : MeasureTheory.SimpleFunc.instSMul = { smul := fun k f => MeasureTheory.SimpleFunc.map (fun x => k • x) f }
• MeasureTheory.SimpleFunc.instVAdd.eq_1 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [VAdd K β] : MeasureTheory.SimpleFunc.instVAdd = { vadd := fun k f => MeasureTheory.SimpleFunc.map (fun x => k +ᵥ x) f }
• MeasureTheory.SimpleFunc.coe_map 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (g : β → γ) (f : MeasureTheory.SimpleFunc α β) : ⇑(MeasureTheory.SimpleFunc.map g f) = g ∘ ⇑f
• MeasureTheory.SimpleFunc.FinMeasSupp.map 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [Zero β] [Zero γ] {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α β} {g : β → γ} (hf : f.FinMeasSupp μ) (hg : g 0 = 0) : (MeasureTheory.SimpleFunc.map g f).FinMeasSupp μ
• MeasureTheory.SimpleFunc.instAdd.eq_1 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Add β] : MeasureTheory.SimpleFunc.instAdd = { add := fun f g => (MeasureTheory.SimpleFunc.map (fun x1 x2 => x1 + x2) f).seq g }
• MeasureTheory.SimpleFunc.instDiv.eq_1 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Div β] : MeasureTheory.SimpleFunc.instDiv = { div := fun f g => (MeasureTheory.SimpleFunc.map (fun x1 x2 => x1 / x2) f).seq g }
• MeasureTheory.SimpleFunc.instMul.eq_1 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Mul β] : MeasureTheory.SimpleFunc.instMul = { mul := fun f g => (MeasureTheory.SimpleFunc.map (fun x1 x2 => x1 * x2) f).seq g }
• MeasureTheory.SimpleFunc.instSub.eq_1 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Sub β] : MeasureTheory.SimpleFunc.instSub = { sub := fun f g => (MeasureTheory.SimpleFunc.map (fun x1 x2 => x1 - x2) f).seq g }
• MeasureTheory.SimpleFunc.FinMeasSupp.of_map 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [Zero β] [Zero γ] {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α β} {g : β → γ} (h : (MeasureTheory.SimpleFunc.map g f).FinMeasSupp μ) (hg : ∀ (b : β), g b = 0 → b = 0) : f.FinMeasSupp μ
• MeasureTheory.SimpleFunc.smul_eq_map 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {K : Type u_5} [SMul K β] (k : K) (f : MeasureTheory.SimpleFunc α β) : k • f = MeasureTheory.SimpleFunc.map (fun x => k • x) f
• MeasureTheory.SimpleFunc.sup_eq_map₂ 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Max β] (f g : MeasureTheory.SimpleFunc α β) : f ⊔ g = MeasureTheory.SimpleFunc.map (fun p => p.1 ⊔ p.2) (f.pair g)
• MeasureTheory.SimpleFunc.FinMeasSupp.map_iff 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [Zero β] [Zero γ] {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α β} {g : β → γ} (hg : ∀ {b : β}, g b = 0 ↔ b = 0) : (MeasureTheory.SimpleFunc.map g f).FinMeasSupp μ ↔ f.FinMeasSupp μ
• MeasureTheory.SimpleFunc.const_add_eq_map 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Add β] (f : MeasureTheory.SimpleFunc α β) (b : β) : MeasureTheory.SimpleFunc.const α b + f = MeasureTheory.SimpleFunc.map (fun a => b + a) f
• MeasureTheory.SimpleFunc.const_mul_eq_map 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Mul β] (f : MeasureTheory.SimpleFunc α β) (b : β) : MeasureTheory.SimpleFunc.const α b * f = MeasureTheory.SimpleFunc.map (fun a => b * a) f
• MeasureTheory.SimpleFunc.map_restrict_of_zero 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [Zero β] [Zero γ] {g : β → γ} (hg : g 0 = 0) (f : MeasureTheory.SimpleFunc α β) (s : Set α) : MeasureTheory.SimpleFunc.map g (f.restrict s) = (MeasureTheory.SimpleFunc.map g f).restrict s
• MeasureTheory.SimpleFunc.eapproxDiff.eq_2 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} [MeasurableSpace α] (f : α → ENNReal) (n : ℕ) : MeasureTheory.SimpleFunc.eapproxDiff f n.succ = MeasureTheory.SimpleFunc.map ENNReal.toNNReal (MeasureTheory.SimpleFunc.eapprox f (n + 1) - MeasureTheory.SimpleFunc.eapprox f n)
• MeasureTheory.SimpleFunc.add_eq_map₂ 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Add β] (f g : MeasureTheory.SimpleFunc α β) : f + g = MeasureTheory.SimpleFunc.map (fun p => p.1 + p.2) (f.pair g)
• MeasureTheory.SimpleFunc.mul_eq_map₂ 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Mul β] (f g : MeasureTheory.SimpleFunc α β) : f * g = MeasureTheory.SimpleFunc.map (fun p => p.1 * p.2) (f.pair g)
• MeasureTheory.SimpleFunc.map_preimage_singleton 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (g : β → γ) (c : γ) : ⇑(MeasureTheory.SimpleFunc.map g f) ⁻¹' {c} = ⇑f ⁻¹' ↑({b ∈ f.range | g b = c})
• MeasureTheory.SimpleFunc.map_preimage 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (g : β → γ) (s : Set γ) : ⇑(MeasureTheory.SimpleFunc.map g f) ⁻¹' s = ⇑f ⁻¹' ↑({b ∈ f.range | g b ∈ s})
• MeasureTheory.SimpleFunc.FinMeasSupp.map₂ 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : MeasurableSpace α} [Zero β] [Zero γ] {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α β} [Zero δ] (hf : f.FinMeasSupp μ) {g : MeasureTheory.SimpleFunc α γ} (hg : g.FinMeasSupp μ) {op : β → γ → δ} (H : op 0 0 = 0) : (MeasureTheory.SimpleFunc.map (Function.uncurry op) (f.pair g)).FinMeasSupp μ
• MeasureTheory.SimpleFunc.map_lintegral 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (g : β → ENNReal) (f : MeasureTheory.SimpleFunc α β) : (MeasureTheory.SimpleFunc.map g f).lintegral μ = ∑ x ∈ f.range, g x * μ (⇑f ⁻¹' {x})
• MeasureTheory.SimpleFunc.map_add 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [Add β] [Add γ] {g : β → γ} (hg : ∀ (x y : β), g (x + y) = g x + g y) (f₁ f₂ : MeasureTheory.SimpleFunc α β) : MeasureTheory.SimpleFunc.map g (f₁ + f₂) = MeasureTheory.SimpleFunc.map g f₁ + MeasureTheory.SimpleFunc.map g f₂
• MeasureTheory.SimpleFunc.map_mul 📋 Mathlib.MeasureTheory.Function.SimpleFunc
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [Mul β] [Mul γ] {g : β → γ} (hg : ∀ (x y : β), g (x * y) = g x * g y) (f₁ f₂ : MeasureTheory.SimpleFunc α β) : MeasureTheory.SimpleFunc.map g (f₁ * f₂) = MeasureTheory.SimpleFunc.map g f₁ * MeasureTheory.SimpleFunc.map g f₂
• MeasureTheory.lintegral_eq_nnreal 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Basic
  {α : Type u_1} {m : MeasurableSpace α} (f : α → ENNReal) (μ : MeasureTheory.Measure α) : ∫⁻ (a : α), f a ∂μ = ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (MeasureTheory.SimpleFunc.map ENNReal.ofNNReal φ).lintegral μ
• MeasureTheory.exists_simpleFunc_forall_lintegral_sub_lt_of_pos 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Basic
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (h : ∫⁻ (x : α), f x ∂μ ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ φ, (∀ (x : α), ↑(φ x) ≤ f x) ∧ ∀ (ψ : MeasureTheory.SimpleFunc α NNReal), (∀ (x : α), ↑(ψ x) ≤ f x) → (MeasureTheory.SimpleFunc.map ENNReal.ofNNReal (ψ - φ)).lintegral μ < ε
• MeasureTheory.SimpleFunc.nearestPt.eq_1 📋 Mathlib.MeasureTheory.Function.SimpleFuncDense
  {α : Type u_1} [MeasurableSpace α] [PseudoEMetricSpace α] [OpensMeasurableSpace α] (e : ℕ → α) (N : ℕ) : MeasureTheory.SimpleFunc.nearestPt e N = MeasureTheory.SimpleFunc.map e (MeasureTheory.SimpleFunc.nearestPtInd e N)
• MeasureTheory.StronglyMeasurable.approxBounded.eq_1 📋 Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
  {α : Type u_1} {β : Type u_2} {f : α → β} [TopologicalSpace β] {x✝ : MeasurableSpace α} [Norm β] [SMul ℝ β] (hf : MeasureTheory.StronglyMeasurable f) (c : ℝ) (n : ℕ) : hf.approxBounded c n = MeasureTheory.SimpleFunc.map (fun x => min 1 (c / ‖x‖) • x) (hf.approx n)
• MeasureTheory.SimpleFunc.map_setToSimpleFunc 📋 Mathlib.MeasureTheory.Integral.FinMeasAdditive
  {α : Type u_1} {F : Type u_3} {F' : Type u_4} {G : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] [NormedAddCommGroup G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (T : Set α → F →L[ℝ] F') (h_add : MeasureTheory.FinMeasAdditive μ T) {f : MeasureTheory.SimpleFunc α G} (hf : MeasureTheory.Integrable (⇑f) μ) {g : G → F} (hg : g 0 = 0) : MeasureTheory.SimpleFunc.setToSimpleFunc T (MeasureTheory.SimpleFunc.map g f) = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (g x)
• MeasureTheory.SimpleFunc.posPart_map_norm 📋 Mathlib.MeasureTheory.Integral.Bochner.L1
  {α : Type u_1} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α ℝ) : MeasureTheory.SimpleFunc.map norm f.posPart = f.posPart
• MeasureTheory.SimpleFunc.negPart_map_norm 📋 Mathlib.MeasureTheory.Integral.Bochner.L1
  {α : Type u_1} [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α ℝ) : MeasureTheory.SimpleFunc.map norm f.negPart = f.negPart
• MeasureTheory.SimpleFunc.posPart.eq_1 📋 Mathlib.MeasureTheory.Integral.Bochner.L1
  {α : Type u_1} {E : Type u_2} [LinearOrder E] [Zero E] [MeasurableSpace α] (f : MeasureTheory.SimpleFunc α E) : f.posPart = MeasureTheory.SimpleFunc.map (fun b => max b 0) f
• MeasureTheory.SimpleFunc.norm_integral_le_integral_norm 📋 Mathlib.MeasureTheory.Integral.Bochner.L1
  {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.Integrable (⇑f) μ) : ‖MeasureTheory.SimpleFunc.integral μ f‖ ≤ MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map norm f)
• MeasureTheory.SimpleFunc.integral_eq_lintegral' 📋 Mathlib.MeasureTheory.Integral.Bochner.L1
  {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α E} {g : E → ENNReal} (hf : MeasureTheory.Integrable (⇑f) μ) (hg0 : g 0 = 0) (ht : ∀ (b : E), g b ≠ ⊤) : MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map (ENNReal.toReal ∘ g) f) = (∫⁻ (a : α), g (f a) ∂μ).toReal
• MeasureTheory.SimpleFunc.map_integral 📋 Mathlib.MeasureTheory.Integral.Bochner.L1
  {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E) (g : E → F) (hf : MeasureTheory.Integrable (⇑f) μ) (hg : g 0 = 0) : MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map g f) = ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • g x
• MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_integral_norm 📋 Mathlib.MeasureTheory.Integral.Bochner.L1
  {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] (T : Set α → E →L[ℝ] F) {C : ℝ} (hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * μ.real s) {f : MeasureTheory.SimpleFunc α E} (hf : MeasureTheory.Integrable (⇑f) μ) : ‖MeasureTheory.SimpleFunc.setToSimpleFunc T f‖ ≤ C * MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map norm f)
• MeasureTheory.L1.SimpleFunc.norm_eq_integral 📋 Mathlib.MeasureTheory.Integral.Bochner.L1
  {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)) : ‖f‖ = MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map norm (MeasureTheory.Lp.simpleFunc.toSimpleFunc f))

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 19971e9 serving mathlib revision bce1d65