Loogle!
Result
Found 46 definitions whose name contains "of_closed".
- Filter.Frequently.mem_of_closed Mathlib.Topology.Basic
∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], (∃ᶠ (x : X) in nhds x, x ∈ s) → IsClosed s → x ∈ s - EMetric.ordConnected_setOf_closedBall_subset Mathlib.Topology.EMetricSpace.Basic
∀ {α : Type u} [inst : PseudoEMetricSpace α] (x : α) (s : Set α), Set.OrdConnected {r | EMetric.closedBall x r ⊆ s} - Metric.mem_of_closed' Mathlib.Topology.MetricSpace.PseudoMetric
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, IsClosed s → ∀ {a : α}, a ∈ s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε - Metric.mem_cocompact_of_closedBall_compl_subset Mathlib.Topology.MetricSpace.Bounded
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} [inst_1 : ProperSpace α] (c : α), (∃ r, (Metric.closedBall c r)ᶜ ⊆ s) → s ∈ Filter.cocompact α - EMetric.mem_iff_infEdist_zero_of_closed Mathlib.Topology.MetricSpace.HausdorffDistance
∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α}, IsClosed s → (x ∈ s ↔ EMetric.infEdist x s = 0) - EMetric.hausdorffEdist_zero_iff_eq_of_closed Mathlib.Topology.MetricSpace.HausdorffDistance
∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α}, IsClosed s → IsClosed t → (EMetric.hausdorffEdist s t = 0 ↔ s = t) - IsNowhereDense.subset_of_closed_isNowhereDense Mathlib.Topology.GDelta
∀ {X : Type u_5} [inst : TopologicalSpace X] {s : Set X}, IsNowhereDense s → ∃ t, s ⊆ t ∧ IsNowhereDense t ∧ IsClosed t - ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness
∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [inst : NormedAddCommGroup F] [inst_1 : NontriviallyNormedField 𝕜] [inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [inst_4 : SeminormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : RingHomIsometric σ₁₂] [inst_7 : ProperSpace F] {s : Set (E' →SL[σ₁₂] F)}, Bornology.IsBounded s → IsClosed (DFunLike.coe '' s) → IsCompact (DFunLike.coe '' s) - dense_iUnion_interior_of_closed Mathlib.Topology.Baire.Lemmas
∀ {X : Type u_1} {ι : Sort u_3} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] [inst_2 : Countable ι] {f : ι → Set X}, (∀ (i : ι), IsClosed (f i)) → ⋃ i, f i = Set.univ → Dense (⋃ i, interior (f i)) - nonempty_interior_of_iUnion_of_closed Mathlib.Topology.Baire.Lemmas
∀ {X : Type u_1} {ι : Sort u_3} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] [inst_2 : Nonempty X] [inst_3 : Countable ι] {f : ι → Set X}, (∀ (i : ι), IsClosed (f i)) → ⋃ i, f i = Set.univ → ∃ i, Set.Nonempty (interior (f i)) - IsGδ.dense_iUnion_interior_of_closed Mathlib.Topology.Baire.Lemmas
∀ {X : Type u_1} {ι : Sort u_3} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] [inst_2 : Countable ι] {s : Set X}, IsGδ s → Dense s → ∀ {f : ι → Set X}, (∀ (i : ι), IsClosed (f i)) → s ⊆ ⋃ i, f i → Dense (⋃ i, interior (f i)) - dense_sUnion_interior_of_closed Mathlib.Topology.Baire.Lemmas
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] {S : Set (Set X)}, (∀ s ∈ S, IsClosed s) → Set.Countable S → ⋃₀ S = Set.univ → Dense (⋃ s ∈ S, interior s) - IsGδ.dense_sUnion_interior_of_closed Mathlib.Topology.Baire.Lemmas
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] {T : Set (Set X)} {s : Set X}, IsGδ s → Dense s → Set.Countable T → (∀ t ∈ T, IsClosed t) → s ⊆ ⋃₀ T → Dense (⋃ t ∈ T, interior t) - dense_biUnion_interior_of_closed Mathlib.Topology.Baire.Lemmas
∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] {S : Set α} {f : α → Set X}, (∀ s ∈ S, IsClosed (f s)) → Set.Countable S → ⋃ s ∈ S, f s = Set.univ → Dense (⋃ s ∈ S, interior (f s)) - IsGδ.dense_biUnion_interior_of_closed Mathlib.Topology.Baire.Lemmas
∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : BaireSpace X] {t : Set α} {s : Set X}, IsGδ s → Dense s → Set.Countable t → ∀ {f : α → Set X}, (∀ i ∈ t, IsClosed (f i)) → s ⊆ ⋃ i ∈ t, f i → Dense (⋃ i ∈ t, interior (f i)) - exists_bounded_mem_Icc_of_closed_of_le Mathlib.Topology.UrysohnsBounded
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : NormalSpace X] {s t : Set X}, IsClosed s → IsClosed t → Disjoint s t → ∀ {a b : ℝ}, a ≤ b → ∃ f, Set.EqOn (⇑f) (Function.const X a) s ∧ Set.EqOn (⇑f) (Function.const X b) t ∧ ∀ (x : X), f x ∈ Set.Icc a b - exists_bounded_zero_one_of_closed Mathlib.Topology.UrysohnsBounded
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : NormalSpace X] {s t : Set X}, IsClosed s → IsClosed t → Disjoint s t → ∃ f, Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1 - ContinuousMap.exists_restrict_eq_of_closed Mathlib.Topology.TietzeExtension
∀ {X : Type u} [inst : TopologicalSpace X] [inst_1 : NormalSpace X] {s : Set X}, IsClosed s → ∀ {Y : Type v} [inst_2 : TopologicalSpace Y] [inst_3 : TietzeExtension Y] (f : C(↑s, Y)), ∃ g, ContinuousMap.restrict s g = f - ContinuousMap.exists_extension_of_closedEmbedding Mathlib.Topology.TietzeExtension
∀ {X₁ : Type u₁} [inst : TopologicalSpace X₁] {X : Type u} [inst_1 : TopologicalSpace X] [inst_2 : NormalSpace X] {e : X₁ → X}, ClosedEmbedding e → ∀ {Y : Type v} [inst_3 : TopologicalSpace Y] [inst_4 : TietzeExtension Y] (f : C(X₁, Y)), ∃ g, ⇑g ∘ e = ⇑f - BoundedContinuousFunction.exists_extension_norm_eq_of_closedEmbedding' Mathlib.Topology.TietzeExtension
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : NormalSpace Y] (f : BoundedContinuousFunction X ℝ) (e : C(X, Y)), ClosedEmbedding ⇑e → ∃ g, ‖g‖ = ‖f‖ ∧ BoundedContinuousFunction.compContinuous g e = f - BoundedContinuousFunction.exists_extension_norm_eq_of_closedEmbedding Mathlib.Topology.TietzeExtension
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : NormalSpace Y] (f : BoundedContinuousFunction X ℝ) {e : X → Y}, ClosedEmbedding e → ∃ g, ‖g‖ = ‖f‖ ∧ ⇑g ∘ e = ⇑f - BoundedContinuousFunction.exists_extension_forall_mem_of_closedEmbedding Mathlib.Topology.TietzeExtension
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : NormalSpace Y] (f : BoundedContinuousFunction X ℝ) {t : Set ℝ} {e : X → Y} [hs : Set.OrdConnected t], (∀ (x : X), f x ∈ t) → Set.Nonempty t → ClosedEmbedding e → ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f - BoundedContinuousFunction.exists_extension_forall_mem_Icc_of_closedEmbedding Mathlib.Topology.TietzeExtension
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : NormalSpace Y] (f : BoundedContinuousFunction X ℝ) {a b : ℝ} {e : X → Y}, (∀ (x : X), f x ∈ Set.Icc a b) → a ≤ b → ClosedEmbedding e → ∃ g, (∀ (y : Y), g y ∈ Set.Icc a b) ∧ ⇑g ∘ e = ⇑f - BoundedContinuousFunction.exists_norm_eq_restrict_eq_of_closed Mathlib.Topology.TietzeExtension
∀ {Y : Type u_2} [inst : TopologicalSpace Y] [inst_1 : NormalSpace Y] {s : Set Y} (f : BoundedContinuousFunction ↑s ℝ), IsClosed s → ∃ g, ‖g‖ = ‖f‖ ∧ BoundedContinuousFunction.restrict g s = f - BoundedContinuousFunction.exists_extension_forall_exists_le_ge_of_closedEmbedding Mathlib.Topology.TietzeExtension
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : NormalSpace Y] [inst_3 : Nonempty X] (f : BoundedContinuousFunction X ℝ) {e : X → Y}, ClosedEmbedding e → ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Set.Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f - BoundedContinuousFunction.exists_forall_mem_restrict_eq_of_closed Mathlib.Topology.TietzeExtension
∀ {Y : Type u_2} [inst : TopologicalSpace Y] [inst_1 : NormalSpace Y] {s : Set Y} (f : BoundedContinuousFunction ↑s ℝ), IsClosed s → ∀ {t : Set ℝ} [inst_2 : Set.OrdConnected t], (∀ (x : ↑s), f x ∈ t) → Set.Nonempty t → ∃ g, (∀ (y : Y), g y ∈ t) ∧ BoundedContinuousFunction.restrict g s = f - ContinuousMap.exists_extension_forall_mem_of_closedEmbedding Mathlib.Topology.TietzeExtension
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : NormalSpace Y] (f : C(X, ℝ)) {t : Set ℝ} {e : X → Y} [hs : Set.OrdConnected t], (∀ (x : X), f x ∈ t) → Set.Nonempty t → ClosedEmbedding e → ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f - ContinuousMap.exists_restrict_eq_forall_mem_of_closed Mathlib.Topology.TietzeExtension
∀ {Y : Type u_2} [inst : TopologicalSpace Y] [inst_1 : NormalSpace Y] {s : Set Y} (f : C(↑s, ℝ)) {t : Set ℝ} [inst_2 : Set.OrdConnected t], (∀ (x : ↑s), f x ∈ t) → Set.Nonempty t → IsClosed s → ∃ g, (∀ (y : Y), g y ∈ t) ∧ ContinuousMap.restrict s g = f - MeasureTheory.exists_continuous_snorm_sub_le_of_closed Mathlib.MeasureTheory.Function.ContinuousMapDense
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [inst_2 : T4Space α] [inst_3 : BorelSpace α] {E : Type u_2} [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_5 : NormedSpace ℝ E] [inst_6 : MeasureTheory.Measure.OuterRegular μ], p ≠ ⊤ → ∀ {s u : Set α}, IsClosed s → IsOpen u → s ⊆ u → ↑↑μ s ≠ ⊤ → ∀ (c : E) {ε : ENNReal}, ε ≠ 0 → ∃ f, Continuous f ∧ MeasureTheory.snorm (fun x => f x - Set.indicator s (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MeasureTheory.Memℒp f p μ - WeakDual.isCompact_of_bounded_of_closed Mathlib.Analysis.NormedSpace.WeakDual
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : ProperSpace 𝕜] {s : Set (WeakDual 𝕜 E)}, Bornology.IsBounded (⇑NormedSpace.Dual.toWeakDual ⁻¹' s) → IsClosed s → IsCompact s - WeakDual.isClosed_image_coe_of_bounded_of_closed Mathlib.Analysis.NormedSpace.WeakDual
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {s : Set (WeakDual 𝕜 E)}, Bornology.IsBounded (⇑NormedSpace.Dual.toWeakDual ⁻¹' s) → IsClosed s → IsClosed (DFunLike.coe '' s) - CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimits Mathlib.CategoryTheory.Limits.FullSubcategory
∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] {P : C → Prop}, CategoryTheory.Limits.ClosedUnderColimitsOfShape J P → ∀ [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C], CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.FullSubcategory P) - CategoryTheory.Limits.hasColimitsOfShape_of_closed_under_colimits Mathlib.CategoryTheory.Limits.FullSubcategory
∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] {P : C → Prop}, CategoryTheory.Limits.ClosedUnderColimitsOfShape J P → ∀ [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C], CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.FullSubcategory P) - CategoryTheory.Limits.hasLimitsOfShape_of_closedUnderLimits Mathlib.CategoryTheory.Limits.FullSubcategory
∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] {P : C → Prop}, CategoryTheory.Limits.ClosedUnderLimitsOfShape J P → ∀ [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C], CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.FullSubcategory P) - CategoryTheory.Limits.hasColimit_of_closedUnderColimits Mathlib.CategoryTheory.Limits.FullSubcategory
∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] {P : C → Prop}, CategoryTheory.Limits.ClosedUnderColimitsOfShape J P → ∀ (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) [inst_2 : CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (CategoryTheory.fullSubcategoryInclusion P))], CategoryTheory.Limits.HasColimit F - CategoryTheory.Limits.hasColimit_of_closed_under_colimits Mathlib.CategoryTheory.Limits.FullSubcategory
∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] {P : C → Prop}, CategoryTheory.Limits.ClosedUnderColimitsOfShape J P → ∀ (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) [inst_2 : CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (CategoryTheory.fullSubcategoryInclusion P))], CategoryTheory.Limits.HasColimit F - CategoryTheory.Limits.hasLimit_of_closedUnderLimits Mathlib.CategoryTheory.Limits.FullSubcategory
∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] {P : C → Prop}, CategoryTheory.Limits.ClosedUnderLimitsOfShape J P → ∀ (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) [inst_2 : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (CategoryTheory.fullSubcategoryInclusion P))], CategoryTheory.Limits.HasLimit F - CategoryTheory.Limits.hasLimit_of_closed_under_limits Mathlib.CategoryTheory.Limits.FullSubcategory
∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] {P : C → Prop}, CategoryTheory.Limits.ClosedUnderLimitsOfShape J P → ∀ (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) [inst_2 : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (CategoryTheory.fullSubcategoryInclusion P))], CategoryTheory.Limits.HasLimit F - CategoryTheory.le_topology_of_closedSieves_isSheaf Mathlib.CategoryTheory.Sites.Closed
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J₁ J₂ : CategoryTheory.GrothendieckTopology C}, CategoryTheory.Presieve.IsSheaf J₁ (CategoryTheory.Functor.closedSieves J₂) → J₁ ≤ J₂ - Complex.subfield_eq_of_closed Mathlib.Topology.Instances.Complex
∀ {K : Subfield ℂ}, IsClosed ↑K → K = RingHom.fieldRange Complex.ofReal ∨ K = ⊤ - isProperMap_of_closedEmbedding Mathlib.Topology.ProperMap
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}, ClosedEmbedding f → IsProperMap f - isProperMap_subtype_val_of_closed Mathlib.Topology.ProperMap
∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X}, IsClosed U → IsProperMap Subtype.val - isProperMap_restr_of_proper_of_closed Mathlib.Topology.ProperMap
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {U : Set X}, IsProperMap f → IsClosed U → IsProperMap fun x => f ↑x - ArzelaAscoli.compactSpace_of_closedEmbedding Mathlib.Topology.UniformSpace.Ascoli
∀ {ι : Type u_1} {X : Type u_2} {α : Type u_4} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α} [inst_2 : TopologicalSpace ι] {𝔖 : Set (Set X)}, (∀ K ∈ 𝔖, IsCompact K) → ClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F) → (∀ K ∈ 𝔖, EquicontinuousOn F K) → (∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q) → CompactSpace ι - ArzelaAscoli.compactSpace_of_closed_inducing' Mathlib.Topology.UniformSpace.Ascoli
∀ {ι : Type u_1} {X : Type u_2} {α : Type u_4} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α} [inst_2 : TopologicalSpace ι] {𝔖 : Set (Set X)}, (∀ K ∈ 𝔖, IsCompact K) → Inducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) → IsClosed (Set.range (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) → (∀ K ∈ 𝔖, EquicontinuousOn F K) → (∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q) → CompactSpace ι - ArzelaAscoli.isCompact_closure_of_closedEmbedding Mathlib.Topology.UniformSpace.Ascoli
∀ {ι : Type u_1} {X : Type u_2} {α : Type u_4} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α} [inst_2 : TopologicalSpace ι] [inst_3 : T2Space α] {𝔖 : Set (Set X)}, (∀ K ∈ 𝔖, IsCompact K) → ClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F) → ∀ {s : Set ι}, (∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K) → (∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q) → IsCompact (closure s)
Did you maybe mean
About
Loogle searches of Lean and Mathlib definitions and theorems.
You may also want to try the CLI version, the 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 currently provided by Joachim Breitner <mail@joachim-breitner.de>.
This is Loogle revision 34713b2
serving mathlib revision a547a94