Loogle!
Result
Found 59 declarations whose name contains "of_compact".
- CompleteLattice.Iic_coatomic_of_compact_element š Mathlib.Order.CompactlyGenerated.Basic
{α : Type u_2} [CompleteLattice α] {k : α} (h : CompleteLattice.IsCompactElement k) : IsCoatomic ā(Set.Iic k) - finite_of_compact_of_discrete š Mathlib.Topology.Compactness.Compact
{X : Type u} [TopologicalSpace X] [CompactSpace X] [DiscreteTopology X] : Finite X - exists_clusterPt_of_compactSpace š Mathlib.Topology.Compactness.Compact
{X : Type u} [TopologicalSpace X] [CompactSpace X] (f : Filter X) [f.NeBot] : ā x, ClusterPt x f - isClosedMap_fst_of_compactSpace š Mathlib.Topology.Compactness.Compact
{X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace Y] : IsClosedMap Prod.fst - isClosedMap_snd_of_compactSpace š Mathlib.Topology.Compactness.Compact
{X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] : IsClosedMap Prod.snd - exists_subset_nhds_of_compactSpace š Mathlib.Topology.Compactness.Compact
{X : Type u} {ι : Type u_1} [TopologicalSpace X] [CompactSpace X] [Nonempty ι] {V : ι ā Set X} (hV : Directed (fun x1 x2 => x1 ā x2) V) (hV_closed : ā (i : ι), IsClosed (V i)) {U : Set X} (hU : ā x ā ā i, V i, U ā nhds x) : ā i, V i ā U - LocallyFinite.finite_nonempty_of_compact š Mathlib.Topology.Compactness.LocallyFinite
{X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [CompactSpace X] {f : ι ā Set X} (hf : LocallyFinite f) : {i | (f i).Nonempty}.Finite - LocallyFinite.finite_of_compact š Mathlib.Topology.Compactness.LocallyFinite
{X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [CompactSpace X] {f : ι ā Set X} (hf : LocallyFinite f) (hne : ā (i : ι), (f i).Nonempty) : Set.univ.Finite - complete_of_compact š Mathlib.Topology.UniformSpace.Cauchy
{α : Type u} [UniformSpace α] [CompactSpace α] : CompleteSpace α - NormalSpace.of_compactSpace_r1Space š Mathlib.Topology.Separation.Regular
{X : Type u_1} [TopologicalSpace X] [CompactSpace X] [R1Space X] : NormalSpace X - unique_uniformity_of_compact š Mathlib.Topology.UniformSpace.Compact
{γ : Type uc} [t : TopologicalSpace γ] [CompactSpace γ] {u u' : UniformSpace γ} (h : u.toTopologicalSpace = t) (h' : u'.toTopologicalSpace = t) : u = u' - lebesgue_number_of_compact_open š Mathlib.Topology.UniformSpace.Compact
{α : Type ua} [UniformSpace α] {K U : Set α} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ā U) : ā V ā uniformity α, IsOpen V ā§ ā x ā K, UniformSpace.ball x V ā U - HasCompactMulSupport.of_compactSpace š Mathlib.Topology.Algebra.Support
{α : Type u_2} {γ : Type u_5} [TopologicalSpace α] [One γ] [CompactSpace α] (f : α ā γ) : HasCompactMulSupport f - HasCompactSupport.of_compactSpace š Mathlib.Topology.Algebra.Support
{α : Type u_2} {γ : Type u_5} [TopologicalSpace α] [Zero γ] [CompactSpace α] (f : α ā γ) : HasCompactSupport f - tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace š Mathlib.Topology.UniformSpace.LocallyUniformConvergence
{α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι ā α ā β} {f : α ā β} {p : Filter ι} [CompactSpace α] : TendstoLocallyUniformly F f p ā TendstoUniformly F f p - tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact š Mathlib.Topology.UniformSpace.LocallyUniformConvergence
{α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {F : ι ā α ā β} {f : α ā β} {s : Set α} {p : Filter ι} (hs : IsCompact s) : TendstoLocallyUniformlyOn F f p s ā TendstoUniformlyOn F f p s - topologicalAddGroup_is_uniform_of_compactSpace š Mathlib.Topology.Algebra.IsUniformGroup.Basic
(G : Type u_1) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [CompactSpace G] : IsUniformAddGroup G - topologicalGroup_is_uniform_of_compactSpace š Mathlib.Topology.Algebra.IsUniformGroup.Basic
(G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] : IsUniformGroup G - EMetric.subset_countable_closure_of_compact š Mathlib.Topology.EMetricSpace.Basic
{α : Type u} [PseudoEMetricSpace α] {s : Set α} (hs : IsCompact s) : ā t ā s, t.Countable ā§ s ā closure t - EMetric.countable_closure_of_compact š Mathlib.Topology.EMetricSpace.Basic
{γ : Type w} [EMetricSpace γ] {s : Set γ} (hs : IsCompact s) : ā t ā s, t.Countable ā§ s = closure t - finite_cover_balls_of_compact š Mathlib.Topology.MetricSpace.Pseudo.Basic
{X : Type u_2} [PseudoMetricSpace X] {s : Set X} (hs : IsCompact s) {e : ā} (he : 0 < e) : ā t ā s, t.Finite ā§ s ā ā x ā t, Metric.ball x e - proper_of_compact š Mathlib.Topology.MetricSpace.ProperSpace
{α : Type u} [PseudoMetricSpace α] [CompactSpace α] : ProperSpace α - Metric.isBounded_of_compactSpace š Mathlib.Topology.MetricSpace.Bounded
{α : Type u} [PseudoMetricSpace α] {s : Set α} [CompactSpace α] : Bornology.IsBounded s - isFiniteMeasure_iff_isFiniteMeasureOnCompacts_of_compactSpace š Mathlib.MeasureTheory.Measure.Typeclasses.Finite
{α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [CompactSpace α] : MeasureTheory.IsFiniteMeasure μ ā MeasureTheory.IsFiniteMeasureOnCompacts μ - MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero š Mathlib.MeasureTheory.Group.Action
(G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {K U : Set α} (hK : IsCompact K) (hμK : μ K ā 0) (hU : IsOpen U) (hne : U.Nonempty) : 0 < μ U - MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero š Mathlib.MeasureTheory.Group.Action
(G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {K U : Set α} (hK : IsCompact K) (hμK : μ K ā 0) (hU : IsOpen U) (hne : U.Nonempty) : 0 < μ U - FirstCountableTopology.seq_compact_of_compact š Mathlib.Topology.Sequences
{X : Type u_1} [TopologicalSpace X] [FirstCountableTopology X] [CompactSpace X] : SeqCompactSpace X - Continuous.bounded_above_of_compact_support š Mathlib.Analysis.Normed.Group.Bounded
{α : Type u_1} {E : Type u_2} [NormedAddGroup E] [TopologicalSpace α] {f : α ā E} (hf : Continuous f) (h : HasCompactSupport f) : ā C, ā (x : α), āf xā ⤠C - MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_compact š Mathlib.MeasureTheory.Group.Measure
{G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [IsTopologicalAddGroup G] [μ.IsAddLeftInvariant] (K : Set G) (hK : IsCompact K) (h : μ K ā 0) : μ.IsOpenPosMeasure - MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_compact š Mathlib.MeasureTheory.Group.Measure
{G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] (K : Set G) (hK : IsCompact K) (h : μ K ā 0) : μ.IsOpenPosMeasure - Filter.HasBasis.compactConvergenceUniformity_of_compact š Mathlib.Topology.UniformSpace.CompactConvergence
{α : Type uā} {β : Type uā} [TopologicalSpace α] [UniformSpace β] [CompactSpace α] {ι : Sort u_1} {p : ι ā Prop} {V : ι ā Set (β à β)} (h : (uniformity β).HasBasis p V) : (uniformity C(α, β)).HasBasis p fun i => {fg | ā (x : α), (fg.1 x, fg.2 x) ā V i} - ContinuousMap.hasBasis_compactConvergenceUniformity_of_compact š Mathlib.Topology.UniformSpace.CompactConvergence
{α : Type uā} {β : Type uā} [TopologicalSpace α] [UniformSpace β] [CompactSpace α] : (uniformity C(α, β)).HasBasis (fun V => V ā uniformity β) fun V => {fg | ā (x : α), (fg.1 x, fg.2 x) ā V} - BoundedContinuousFunction.dist_lt_iff_of_compact š Mathlib.Topology.ContinuousMap.Bounded.Basic
{α : Type u} {β : Type v} [TopologicalSpace α] [PseudoMetricSpace β] {f g : BoundedContinuousFunction α β} {C : ā} [CompactSpace α] (C0 : 0 < C) : dist f g < C ā ā (x : α), dist (f x) (g x) < C - BoundedContinuousFunction.norm_lt_iff_of_compact š Mathlib.Topology.ContinuousMap.Bounded.Normed
{α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [CompactSpace α] {f : BoundedContinuousFunction α β} {M : ā} (M0 : 0 < M) : āfā < M ā ā (x : α), āf xā < M - ContinuousMap.linearIsometryBoundedOfCompact_of_compact_toEquiv š Mathlib.Topology.ContinuousMap.Compact
{α : Type u_1} {E : Type u_3} [TopologicalSpace α] [CompactSpace α] [SeminormedAddCommGroup E] {š : Type u_4} [NormedRing š] [Module š E] [IsBoundedSMul š E] : (ContinuousMap.linearIsometryBoundedOfCompact α E š).toEquiv = ContinuousMap.equivBoundedOfCompact α E - continuousOn_integral_of_compact_support š Mathlib.MeasureTheory.Integral.Bochner.Set
{Y : Type u_2} {E : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure Y} [NormedAddCommGroup E] [NormedSpace ā E] {f : X ā Y ā E} {s : Set X} {k : Set Y} [MeasureTheory.IsFiniteMeasureOnCompacts μ] (hk : IsCompact k) (hf : ContinuousOn (Function.uncurry f) (s ĆĖ¢ Set.univ)) (hfs : ā (p : X) (x : Y), p ā s ā x ā k ā f p x = 0) : ContinuousOn (fun x => ā« (y : Y), f x y āμ) s - continuousOn_integral_bilinear_of_locally_integrable_of_compact_support š Mathlib.MeasureTheory.Integral.Bochner.Set
{Y : Type u_2} {E : Type u_3} {F : Type u_4} {X : Type u_5} {G : Type u_6} {š : Type u_7} [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure Y} [NontriviallyNormedField š] [NormedAddCommGroup E] [NormedSpace ā E] [NormedAddCommGroup F] [NormedSpace š F] [NormedAddCommGroup G] [NormedSpace š G] [NormedSpace š E] (L : F āL[š] G āL[š] E) {f : X ā Y ā G} {s : Set X} {k : Set Y} {g : Y ā F} (hk : IsCompact k) (hf : ContinuousOn (Function.uncurry f) (s ĆĖ¢ Set.univ)) (hfs : ā (p : X) (x : Y), p ā s ā x ā k ā f p x = 0) (hg : MeasureTheory.IntegrableOn g k μ) : ContinuousOn (fun x => ā« (y : Y), (L (g y)) (f x y) āμ) s - AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace š Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
{X Y : AlgebraicGeometry.Scheme} (f : X ā¶ Y) [AlgebraicGeometry.QuasiCompact f] [CompactSpace ā„Y] : CompactSpace ā„X - ContinuousMap.induction_on_of_compact š Mathlib.Topology.ContinuousMap.StoneWeierstrass
{š : Type u_1} [RCLike š] {s : Set š} [CompactSpace ās] {p : C(ās, š) ā Prop} (const : ā (r : š), p (ContinuousMap.const (ās) r)) (id : p (ContinuousMap.restrict s (ContinuousMap.id š))) (star_id : p (star (ContinuousMap.restrict s (ContinuousMap.id š)))) (add : ā (f g : C(ās, š)), p f ā p g ā p (f + g)) (mul : ā (f g : C(ās, š)), p f ā p g ā p (f * g)) (frequently : ā (f : C(ās, š)), (āį¶ (g : C(ās, š)) in nhds f, p g) ā p f) (f : C(ās, š)) : p f - ContinuousMapZero.induction_on_of_compact š Mathlib.Topology.ContinuousMap.StoneWeierstrass
{š : Type u_1} [RCLike š] {s : Set š} [Zero ās] (h0 : ā0 = 0) [CompactSpace ās] {p : ContinuousMapZero (ās) š ā Prop} (zero : p 0) (id : p (ContinuousMapZero.id h0)) (star_id : p (star (ContinuousMapZero.id h0))) (add : ā (f g : ContinuousMapZero (ās) š), p f ā p g ā p (f + g)) (mul : ā (f g : ContinuousMapZero (ās) š), p f ā p g ā p (f * g)) (smul : ā (r : š) (f : ContinuousMapZero (ās) š), p f ā p (r ⢠f)) (frequently : ā (f : ContinuousMapZero (ās) š), (āį¶ (g : ContinuousMapZero (ās) š) in nhds f, p g) ā p f) (f : ContinuousMapZero (ās) š) : p f - MeasureTheory.Measure.isAddInvariant_eq_smul_of_compactSpace š Mathlib.MeasureTheory.Measure.Haar.Unique
{G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [CompactSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ'.IsAddLeftInvariant] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] : μ' = μ'.addHaarScalarFactor μ ⢠μ - MeasureTheory.Measure.isMulInvariant_eq_smul_of_compactSpace š Mathlib.MeasureTheory.Measure.Haar.Unique
{G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [CompactSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [μ'.IsMulLeftInvariant] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] : μ' = μ'.haarScalarFactor μ ⢠μ - paracompact_of_compact š Mathlib.Topology.Compactness.Paracompact
{X : Type v} [TopologicalSpace X] [CompactSpace X] : ParacompactSpace X - TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system š Mathlib.Topology.Category.TopCat.Limits.Konig
{J : Type u} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat) [CategoryTheory.IsCofilteredOrEmpty J] [ā (j : J), Nonempty ā(F.obj j)] [ā (j : J), CompactSpace ā(F.obj j)] [ā (j : J), T2Space ā(F.obj j)] : Nonempty ā(TopCat.limitCone F).pt - exists_idempotent_of_compact_t2_of_continuous_add_left š Mathlib.Topology.Algebra.Semigroup
{M : Type u_1} [Nonempty M] [AddSemigroup M] [TopologicalSpace M] [CompactSpace M] [T2Space M] (continuous_mul_left : ā (r : M), Continuous fun x => x + r) : ā m, m + m = m - exists_idempotent_of_compact_t2_of_continuous_mul_left š Mathlib.Topology.Algebra.Semigroup
{M : Type u_1} [Nonempty M] [Semigroup M] [TopologicalSpace M] [CompactSpace M] [T2Space M] (continuous_mul_left : ā (r : M), Continuous fun x => x * r) : ā m, m * m = m - of_compactlyCoherentSpace_of_t2 š Mathlib.Topology.Compactness.CompactlyGeneratedSpace
{X : Type u} [TopologicalSpace X] [T2Space X] [CompactlyCoherentSpace X] : CompactlyGeneratedSpace X - MDifferentiable.apply_eq_of_compactSpace š Mathlib.Geometry.Manifold.Complex
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace ā E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ā F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ā E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [CompactSpace M] [PreconnectedSpace M] {f : M ā F} (hf : MDifferentiable I (modelWithCornersSelf ā F) f) (a b : M) : f a = f b - MDifferentiable.exists_eq_const_of_compactSpace š Mathlib.Geometry.Manifold.Complex
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace ā E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ā F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ā E H} [I.Boundaryless] {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [CompactSpace M] [PreconnectedSpace M] {f : M ā F} (hf : MDifferentiable I (modelWithCornersSelf ā F) f) : ā v, f = Function.const M v - exists_embedding_euclidean_of_compact š Mathlib.Geometry.Manifold.WhitneyEmbedding
{E : Type uE} [NormedAddCommGroup E] [NormedSpace ā E] [FiniteDimensional ā E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ā E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (āā¤) M] [T2Space M] [CompactSpace M] : ā n e, ContMDiff I (modelWithCornersSelf ā (EuclideanSpace ā (Fin n))) (āā¤) e ā§ Topology.IsClosedEmbedding e ā§ ā (x : M), Function.Injective ā(mfderiv I (modelWithCornersSelf ā (EuclideanSpace ā (Fin n))) e x) - CompactlySupportedContinuousMapClass.of_compactSpace š Mathlib.Topology.ContinuousMap.CompactlySupported
{α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Zero β] [TopologicalSpace β] (G : Type u_5) [FunLike G α β] [ContinuousMapClass G α β] [CompactSpace α] : CompactlySupportedContinuousMapClass G α β - MeasureTheory.IsTightMeasureSet.of_compactSpace š Mathlib.MeasureTheory.Measure.Tight
{š§ : Type u_1} [TopologicalSpace š§] {mš§ : MeasurableSpace š§} {S : Set (MeasureTheory.Measure š§)} [CompactSpace š§] : MeasureTheory.IsTightMeasureSet S - IsArtinianRing.finite_of_compactSpace_of_t2Space š Mathlib.Topology.Algebra.Ring.Compact
{R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsArtinianRing R] : Finite R - IsLocalRing.finite_residueField_of_compactSpace š Mathlib.Topology.Algebra.Ring.Compact
{R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsLocalRing R] [IsNoetherianRing R] : Finite (IsLocalRing.ResidueField R) - Valued.integer.isDiscreteValuationRing_of_compactSpace š Mathlib.Topology.Algebra.Valued.LocallyCompact
{K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [h : CompactSpace ā„(Valued.integer K)] : IsDiscreteValuationRing ā„(Valued.integer K) - Valued.integer.isPrincipalIdealRing_of_compactSpace š Mathlib.Topology.Algebra.Valued.LocallyCompact
{F : Type u_2} {Īā : Type u_3} [Field F] [LinearOrderedCommGroupWithZero Īā] [MulArchimedean Īā] [hv : Valued F Īā] [CompactSpace ā„(Valued.integer F)] (h : ā x, 0 < Valued.v x ā§ Valued.v x < 1) : IsPrincipalIdealRing ā„(Valued.integer F) - norm_lt_iff_of_compactlySupported š Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
{α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] {f : BoundedContinuousFunction α γ} (h : f ā compactlySupported α γ) {M : ā} (M0 : 0 < M) : āfā < M ā ā (x : α), āf xā < M - isClosedMap_restrict_of_compactSpace š Mathlib.Topology.IsClosedRestrict
{ι : Type u_1} {α : ι ā Type u_2} {S : Set ι} [(i : ι) ā TopologicalSpace (α i)] [ā (i : ι), CompactSpace (α i)] : IsClosedMap S.restrict - TopologicalSpace.exists_finite_open_cover_prod_subset_of_mem_nhds_diagonal_of_compact š Mathlib.Topology.Separation.DisjointCover
{X : Type u_1} [TopologicalSpace X] {S : Set (X Ć X)} [CompactSpace X] (hS : S ā nhdsSet (Set.diagonal X)) : ā t U, TopologicalSpace.IsOpenCover U ā§ ā (i : { x // x ā t }), ā(U i) ĆĖ¢ ā(U i) ā S
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 findtsum_lt_tsum
even though the hypothesisf 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 07d4605
serving mathlib revision 2e2176e