Loogle!
Result
Found 51 definitions 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 - LocallyFinite.finite_nonempty_of_compact š Mathlib.Topology.Compactness.Compact
{X : Type u} {Ī¹ : Type u_1} [TopologicalSpace X] [CompactSpace X] {f : Ī¹ ā Set X} (hf : LocallyFinite f) : {i | (f i).Nonempty}.Finite - LocallyFinite.finite_of_compact š Mathlib.Topology.Compactness.Compact
{X : Type u} {Ī¹ : Type u_1} [TopologicalSpace X] [CompactSpace X] {f : Ī¹ ā Set X} (hf : LocallyFinite f) (hne : ā (i : Ī¹), (f i).Nonempty) : Set.univ.Finite - 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 - 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 - 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 - 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 - 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
{Ī± : 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.norm_lt_iff_of_compact š Mathlib.Topology.ContinuousMap.Bounded.Basic
{Ī± : Type u} {Ī² : Type v} [TopologicalSpace Ī±] [SeminormedAddCommGroup Ī²] [CompactSpace Ī±] {f : BoundedContinuousFunction Ī± Ī²} {M : ā} (M0 : 0 < M) : āfā < M ā ā (x : Ī±), āf xā < M - 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 - 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.SetIntegral
{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.SetIntegral
{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 - 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 - 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
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, _ * _, _ ^ _, |- _ < _ ā _
woould 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 d56dbe9
serving mathlib revision dbd7065