Loogle!

Result

Found 57 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
• NormalSpace.of_compactSpace_r1Space 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [R1Space X] : NormalSpace X
• 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
• unique_uniformity_of_compact 📋 Mathlib.Topology.UniformSpace.Compact
  {γ : Type uc} [t : TopologicalSpace γ] [CompactSpace γ] {u u' : UniformSpace γ} (h : UniformSpace.toTopologicalSpace = t) (h' : UniformSpace.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
• complete_of_compact 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [UniformSpace α] [CompactSpace α] : CompleteSpace α
• tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace 📋 Mathlib.Topology.UniformSpace.UniformConvergence
  {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [TopologicalSpace α] [CompactSpace α] : TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p
• tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact 📋 Mathlib.Topology.UniformSpace.UniformConvergence
  {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [TopologicalSpace α] (hs : IsCompact s) : TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s
• 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
• 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
• 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
• 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} [NormedField 𝕜] [NormedSpace 𝕜 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
• 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
• AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace 📋 Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] [CompactSpace ↑↑Y.toPresheafedSpace] : CompactSpace ↑↑X.toPresheafedSpace
• 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
• 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:

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 b340a5b serving mathlib revision 5fd096b