Loogle!

Result

Found 51 definitions whose name contains "of_closed".

• Filter.Frequently.mem_of_closed 📋 Mathlib.Topology.Basic
  {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] (h : ∃ᶠ (x : X) in nhds x, x ∈ s) (hs : IsClosed s) : x ∈ s
• EMetric.ordConnected_setOf_closedBall_subset 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [PseudoEMetricSpace α] (x : α) (s : Set α) : {r | EMetric.closedBall x r ⊆ s}.OrdConnected
• Metric.mem_of_closed' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : IsClosed s) {a : α} : a ∈ s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε
• Metric.mem_cocompact_of_closedBall_compl_subset 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} [PseudoMetricSpace α] {s : Set α} [ProperSpace α] (c : α) (h : ∃ r, (Metric.closedBall c r)ᶜ ⊆ s) : s ∈ Filter.cocompact α
• Real.subfield_eq_of_closed 📋 Mathlib.Topology.Instances.Real
  {K : Subfield ℝ} (hc : IsClosed ↑K) : K = ⊤
• EMetric.mem_iff_infEdist_zero_of_closed 📋 Mathlib.Topology.MetricSpace.HausdorffDistance
  {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} (h : IsClosed s) : x ∈ s ↔ EMetric.infEdist x s = 0
• EMetric.hausdorffEdist_zero_iff_eq_of_closed 📋 Mathlib.Topology.MetricSpace.HausdorffDistance
  {α : Type u} [PseudoEMetricSpace α] {s t : Set α} (hs : IsClosed s) (ht : IsClosed t) : EMetric.hausdorffEdist s t = 0 ↔ s = t
• IsNowhereDense.subset_of_closed_isNowhereDense 📋 Mathlib.Topology.GDelta.Basic
  {X : Type u_5} [TopologicalSpace X] {s : Set X} (hs : IsNowhereDense s) : ∃ t, s ⊆ t ∧ IsNowhereDense t ∧ IsClosed t
• isProperMap_of_closedEmbedding 📋 Mathlib.Topology.Maps.Proper.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsClosedEmbedding f) : IsProperMap f
• isProperMap_subtype_val_of_closed 📋 Mathlib.Topology.Maps.Proper.Basic
  {X : Type u_1} [TopologicalSpace X] {C : Set X} (hC : IsClosed C) : IsProperMap Subtype.val
• isProperMap_restr_of_proper_of_closed 📋 Mathlib.Topology.Maps.Proper.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {C : Set X} (hf : IsProperMap f) (hC : IsClosed C) : IsProperMap fun x => f ↑x
• ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image 📋 Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness
  {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] [ProperSpace F] {s : Set (E' →SL[σ₁₂] F)} (hb : Bornology.IsBounded s) (hc : IsClosed (DFunLike.coe '' s)) : IsCompact (DFunLike.coe '' s)
• dense_iUnion_interior_of_closed 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} {ι : Sort u_3} [TopologicalSpace X] [BaireSpace X] [Countable ι] {f : ι → Set X} (hc : ∀ (i : ι), IsClosed (f i)) (hU : ⋃ 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} [TopologicalSpace X] [BaireSpace X] [Nonempty X] [Countable ι] {f : ι → Set X} (hc : ∀ (i : ι), IsClosed (f i)) (hU : ⋃ i, f i = Set.univ) : ∃ i, (interior (f i)).Nonempty
• IsGδ.dense_iUnion_interior_of_closed 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} {ι : Sort u_3} [TopologicalSpace X] [BaireSpace X] [Countable ι] {s : Set X} (hs : IsGδ s) (hd : Dense s) {f : ι → Set X} (hc : ∀ (i : ι), IsClosed (f i)) (hU : s ⊆ ⋃ i, f i) : Dense (⋃ i, interior (f i))
• dense_sUnion_interior_of_closed 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {S : Set (Set X)} (hc : ∀ s ∈ S, IsClosed s) (hS : S.Countable) (hU : ⋃₀ S = Set.univ) : Dense (⋃ s ∈ S, interior s)
• IsGδ.dense_sUnion_interior_of_closed 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {T : Set (Set X)} {s : Set X} (hs : IsGδ s) (hd : Dense s) (hc : T.Countable) (hc' : ∀ t ∈ T, IsClosed t) (hU : s ⊆ ⋃₀ T) : Dense (⋃ t ∈ T, interior t)
• dense_biUnion_interior_of_closed 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} {α : Type u_2} [TopologicalSpace X] [BaireSpace X] {S : Set α} {f : α → Set X} (hc : ∀ s ∈ S, IsClosed (f s)) (hS : S.Countable) (hU : ⋃ 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} [TopologicalSpace X] [BaireSpace X] {t : Set α} {s : Set X} (hs : IsGδ s) (hd : Dense s) (ht : t.Countable) {f : α → Set X} (hc : ∀ i ∈ t, IsClosed (f i)) (hU : s ⊆ ⋃ i ∈ t, f i) : Dense (⋃ i ∈ t, interior (f i))
• AlgebraicGeometry.Scheme.preimage_eq_top_of_closedPoint_mem 📋 Mathlib.AlgebraicGeometry.Stalk
  {X : AlgebraicGeometry.Scheme} {R : CommRingCat} [IsLocalRing ↑R] (f : AlgebraicGeometry.Spec R ⟶ X) {U : X.Opens} (hU : f.base (IsLocalRing.closedPoint ↑R) ∈ U) : (TopologicalSpace.Opens.map f.base).obj U = ⊤
• WeakDual.isCompact_of_bounded_of_closed 📋 Mathlib.Analysis.Normed.Module.WeakDual
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [ProperSpace 𝕜] {s : Set (WeakDual 𝕜 E)} (hb : Bornology.IsBounded (⇑NormedSpace.Dual.toWeakDual ⁻¹' s)) (hc : IsClosed s) : IsCompact s
• WeakDual.isClosed_image_coe_of_bounded_of_closed 📋 Mathlib.Analysis.Normed.Module.WeakDual
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set (WeakDual 𝕜 E)} (hb : Bornology.IsBounded (⇑NormedSpace.Dual.toWeakDual ⁻¹' s)) (hc : IsClosed s) : IsClosed (DFunLike.coe '' s)
• exists_bounded_mem_Icc_of_closed_of_le 📋 Mathlib.Topology.UrysohnsBounded
  {X : Type u_1} [TopologicalSpace X] [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) {a b : ℝ} (hle : 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} [TopologicalSpace X] [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : ∃ f, Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
• ContinuousMap.exists_extension_of_closedEmbedding 📋 Mathlib.Topology.TietzeExtension
  {X₁ : Type u₁} [TopologicalSpace X₁] {X : Type u} [TopologicalSpace X] [NormalSpace X] {e : X₁ → X} {Y : Type v} [TopologicalSpace Y] [TietzeExtension Y] (he : Topology.IsClosedEmbedding e) (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} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : BoundedContinuousFunction X ℝ) (e : C(X, Y)) (he : Topology.IsClosedEmbedding ⇑e) : ∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
• BoundedContinuousFunction.exists_extension_norm_eq_of_closedEmbedding 📋 Mathlib.Topology.TietzeExtension
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : BoundedContinuousFunction X ℝ) {e : X → Y} (he : Topology.IsClosedEmbedding 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} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : BoundedContinuousFunction X ℝ) {t : Set ℝ} {e : X → Y} [hs : t.OrdConnected] (hf : ∀ (x : X), f x ∈ t) (hne : t.Nonempty) (he : Topology.IsClosedEmbedding 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} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : BoundedContinuousFunction X ℝ) {a b : ℝ} {e : X → Y} (hf : ∀ (x : X), f x ∈ Set.Icc a b) (hle : a ≤ b) (he : Topology.IsClosedEmbedding 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} [TopologicalSpace Y] [NormalSpace Y] {s : Set Y} (f : BoundedContinuousFunction ↑s ℝ) (hs : IsClosed s) : ∃ g, ‖g‖ = ‖f‖ ∧ g.restrict s = f
• BoundedContinuousFunction.exists_extension_forall_exists_le_ge_of_closedEmbedding 📋 Mathlib.Topology.TietzeExtension
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] [Nonempty X] (f : BoundedContinuousFunction X ℝ) {e : X → Y} (he : Topology.IsClosedEmbedding 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} [TopologicalSpace Y] [NormalSpace Y] {s : Set Y} (f : BoundedContinuousFunction ↑s ℝ) (hs : IsClosed s) {t : Set ℝ} [t.OrdConnected] (hf : ∀ (x : ↑s), f x ∈ t) (hne : t.Nonempty) : ∃ g, (∀ (y : Y), g y ∈ t) ∧ g.restrict s = f
• ContinuousMap.exists_extension_forall_mem_of_closedEmbedding 📋 Mathlib.Topology.TietzeExtension
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] (f : C(X, ℝ)) {t : Set ℝ} {e : X → Y} [hs : t.OrdConnected] (hf : ∀ (x : X), f x ∈ t) (hne : t.Nonempty) (he : Topology.IsClosedEmbedding 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} [TopologicalSpace Y] [NormalSpace Y] {s : Set Y} (f : C(↑s, ℝ)) {t : Set ℝ} [t.OrdConnected] (ht : ∀ (x : ↑s), f x ∈ t) (hne : t.Nonempty) (hs : IsClosed s) : ∃ g, (∀ (y : Y), g y ∈ t) ∧ ContinuousMap.restrict s g = f
• MeasureTheory.exists_continuous_eLpNorm_sub_le_of_closed 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
  {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace ℝ E] [μ.OuterRegular] (hp : p ≠ ⊤) {s u : Set α} (s_closed : IsClosed s) (u_open : IsOpen u) (hsu : s ⊆ u) (hs : μ s ≠ ⊤) (c : E) {ε : ENNReal} (hε : ε ≠ 0) : ∃ f, Continuous f ∧ MeasureTheory.eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MeasureTheory.Memℒp f p μ
• MeasureTheory.exists_continuous_snorm_sub_le_of_closed 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
  {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace ℝ E] [μ.OuterRegular] (hp : p ≠ ⊤) {s u : Set α} (s_closed : IsClosed s) (u_open : IsOpen u) (hsu : s ⊆ u) (hs : μ s ≠ ⊤) (c : E) {ε : ENNReal} (hε : ε ≠ 0) : ∃ f, Continuous f ∧ MeasureTheory.eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧ (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MeasureTheory.Memℒp f p μ
• CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimits 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderColimitsOfShape J P) [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} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderColimitsOfShape J P) [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.FullSubcategory P)
• CategoryTheory.Limits.hasLimitsOfShape_of_closedUnderLimits 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderLimitsOfShape J P) [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.FullSubcategory P)
• CategoryTheory.Limits.hasColimit_of_closedUnderColimits 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderColimitsOfShape J P) (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.fullSubcategoryInclusion P))] : CategoryTheory.Limits.HasColimit F
• CategoryTheory.Limits.hasColimit_of_closed_under_colimits 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderColimitsOfShape J P) (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.fullSubcategoryInclusion P))] : CategoryTheory.Limits.HasColimit F
• CategoryTheory.Limits.hasLimit_of_closedUnderLimits 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderLimitsOfShape J P) (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) [CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.fullSubcategoryInclusion P))] : CategoryTheory.Limits.HasLimit F
• CategoryTheory.Limits.hasLimit_of_closed_under_limits 📋 Mathlib.CategoryTheory.Limits.FullSubcategory
  {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderLimitsOfShape J P) (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) [CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.fullSubcategoryInclusion P))] : CategoryTheory.Limits.HasLimit F
• CategoryTheory.MorphismProperty.Comma.hasLimitsOfShape_of_closedUnderLimitsOfShape 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
  {T : Type u_1} [CategoryTheory.Category.{u_8, u_1} T] (P : CategoryTheory.MorphismProperty T) {A : Type u_2} {B : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_6, u_2} A] [CategoryTheory.Category.{u_7, u_3} B] [CategoryTheory.Category.{u_5, u_4} J] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} [CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Comma L R)] (h : CategoryTheory.Limits.ClosedUnderLimitsOfShape J fun f => P f.hom) : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.MorphismProperty.Comma L R P ⊤ ⊤)
• CategoryTheory.MorphismProperty.Comma.hasLimit_of_closedUnderLimitsOfShape 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
  {T : Type u_1} [CategoryTheory.Category.{u_8, u_1} T] (P : CategoryTheory.MorphismProperty T) {A : Type u_2} {B : Type u_3} {J : Type u_4} [CategoryTheory.Category.{u_6, u_2} A] [CategoryTheory.Category.{u_7, u_3} B] [CategoryTheory.Category.{u_5, u_4} J] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (D : CategoryTheory.Functor J (CategoryTheory.MorphismProperty.Comma L R P ⊤ ⊤)) (h : CategoryTheory.Limits.ClosedUnderLimitsOfShape J fun f => P f.hom) [CategoryTheory.Limits.HasLimit (D.comp (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤))] : CategoryTheory.Limits.HasLimit D
• CategoryTheory.le_topology_of_closedSieves_isSheaf 📋 Mathlib.CategoryTheory.Sites.Closed
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J₁ J₂ : CategoryTheory.GrothendieckTopology C} (h : CategoryTheory.Presieve.IsSheaf J₁ (CategoryTheory.Functor.closedSieves J₂)) : J₁ ≤ J₂
• Complex.subfield_eq_of_closed 📋 Mathlib.Topology.Instances.Complex
  {K : Subfield ℂ} (hc : IsClosed ↑K) : K = Complex.ofRealHom.fieldRange ∨ K = ⊤
• ArzelaAscoli.compactSpace_of_closedEmbedding 📋 Mathlib.Topology.UniformSpace.Ascoli
  {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [TopologicalSpace ι] {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_clemb : Topology.IsClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) (F_pointwiseCompact : ∀ 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_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [TopologicalSpace ι] {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_ind : Topology.IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) (F_cl : IsClosed (Set.range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) (F_pointwiseCompact : ∀ 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_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [TopologicalSpace ι] [T2Space α] {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_clemb : Topology.IsClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) {s : Set ι} (s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K) (s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q) : IsCompact (closure s)
• properSMul_of_closedEmbedding 📋 Mathlib.Topology.Algebra.ProperAction.Basic
  {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace G] [TopologicalSpace X] {H : Type u_3} [Group H] [MulAction H X] [TopologicalSpace H] [ProperSMul G X] (f : H →* G) (f_clemb : Topology.IsClosedEmbedding ⇑f) (f_compat : ∀ (h : H) (x : X), f h • x = h • x) : ProperSMul H X

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, _ * _, _ ^ _, |- _ < _ → _
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 4e1aab0 serving mathlib revision b513113