Loogle!

Result

Found 122 declarations mentioning CompactSpace and T2Space.

• Continuous.isClosedMap 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : X → Y} (h : Continuous f) : IsClosedMap f
• Continuous.isClosedEmbedding 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : X → Y} (h : Continuous f) (hf : Function.Injective f) : Topology.IsClosedEmbedding f
• IsQuotientMap.of_surjective_continuous 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : X → Y} (hsurj : Function.Surjective f) (hcont : Continuous f) : Topology.IsQuotientMap f
• IsCompact.preimage_continuous 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : X → Y} {s : Set Y} (hs : IsCompact s) (hf : Continuous f) : IsCompact (f ⁻¹' s)
• Ultrafilter.lim_eq_iff_le_nhds 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] {x : X} {F : Ultrafilter X} : F.lim = x ↔ ↑F ≤ nhds x
• isOpen_iff_ultrafilter' 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] (U : Set X) : IsOpen U ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
• ConnectedComponents.t2 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] : T2Space (ConnectedComponents X)
• connectedComponent_eq_iInter_isClopen 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] (x : X) : connectedComponent x = ⋂ s, ↑s
• isHomeomorph_iff_continuous_bijective 📋 Mathlib.Topology.Homeomorph.Lemmas
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [CompactSpace X] [T2Space Y] : IsHomeomorph f ↔ Continuous f ∧ Function.Bijective f
• Continuous.homeoOfEquivCompactToT2 📋 Mathlib.Topology.Homeomorph.Lemmas
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : X ≃ Y} (hf : Continuous ⇑f) : X ≃ₜ Y
• Continuous.toEquiv_homeoOfEquivCompactToT2 📋 Mathlib.Topology.Homeomorph.Lemmas
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : X ≃ Y} (hf : Continuous ⇑f) : hf.homeoOfEquivCompactToT2.toEquiv = f
• Continuous.continuous_symm_of_equiv_compact_to_t2 📋 Mathlib.Topology.Homeomorph.Lemmas
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : X ≃ Y} (hf : Continuous ⇑f) : Continuous ⇑f.symm
• Continuous.isProperMap 📋 Mathlib.Topology.Maps.Proper.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [CompactSpace X] [T2Space Y] (hf : Continuous f) : IsProperMap f
• DivisionRing.finite_of_compactSpace_of_t2Space 📋 Mathlib.Topology.Algebra.Field
  {K : Type u_2} [DivisionRing K] [TopologicalSpace K] [IsTopologicalRing K] [CompactSpace K] [T2Space K] : Finite K
• TopologicalSpace.CompactOpens.instBooleanAlgebra 📋 Mathlib.Topology.Sets.Compacts
  {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [T2Space α] : BooleanAlgebra (TopologicalSpace.CompactOpens α)
• TopologicalSpace.CompactOpens.instCompl 📋 Mathlib.Topology.Sets.Compacts
  {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [T2Space α] : Compl (TopologicalSpace.CompactOpens α)
• TopologicalSpace.CompactOpens.instHImp 📋 Mathlib.Topology.Sets.Compacts
  {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [T2Space α] : HImp (TopologicalSpace.CompactOpens α)
• TopologicalSpace.CompactOpens.coe_compl 📋 Mathlib.Topology.Sets.Compacts
  {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [T2Space α] (s : TopologicalSpace.CompactOpens α) : ↑sᶜ = (↑s)ᶜ
• TopologicalSpace.CompactOpens.coe_himp 📋 Mathlib.Topology.Sets.Compacts
  {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [T2Space α] (s t : TopologicalSpace.CompactOpens α) : ↑(s ⇨ t) = ↑s ⇨ ↑t
• ContinuousMap.algHom_ext_map_X 📋 Mathlib.Topology.ContinuousMap.StoneWeierstrass
  {A : Type u_1} [Semiring A] [Algebra ℝ A] [TopologicalSpace A] [T2Space A] {s : Set ℝ} [CompactSpace ↑s] {φ ψ : C(↑s, ℝ) →ₐ[ℝ] A} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X)) : φ = ψ
• ContinuousMap.starAlgHom_ext_map_X 📋 Mathlib.Topology.ContinuousMap.StoneWeierstrass
  {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [Ring A] [StarRing A] [Algebra 𝕜 A] [TopologicalSpace A] [T2Space A] {s : Set 𝕜} [CompactSpace ↑s] {φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) (h : φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X)) : φ = ψ
• ContinuousMapZero.mul_nonUnitalStarAlgHom_apply_eq_zero 📋 Mathlib.Topology.ContinuousMap.StoneWeierstrass
  {𝕜 : Type u_2} {A : Type u_3} [RCLike 𝕜] [NonUnitalSemiring A] [Star A] [TopologicalSpace A] [SeparatelyContinuousMul A] [T2Space A] [DistribMulAction 𝕜 A] [SMulCommClass 𝕜 A A] {s : Set 𝕜} [Fact (0 ∈ s)] [CompactSpace ↑s] (φ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A) (a : A) (hmul_id : a * φ (ContinuousMapZero.id s) = 0) (hmul_star_id : a * φ (star (ContinuousMapZero.id s)) = 0) (hφ : Continuous ⇑φ) (f : ContinuousMapZero (↑s) 𝕜) : a * φ f = 0
• ContinuousMapZero.nonUnitalStarAlgHom_apply_mul_eq_zero 📋 Mathlib.Topology.ContinuousMap.StoneWeierstrass
  {𝕜 : Type u_2} {A : Type u_3} [RCLike 𝕜] [NonUnitalSemiring A] [Star A] [TopologicalSpace A] [SeparatelyContinuousMul A] [T2Space A] [DistribMulAction 𝕜 A] [IsScalarTower 𝕜 A A] {s : Set 𝕜} [Fact (0 ∈ s)] [CompactSpace ↑s] (φ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A) (a : A) (hmul_id : φ (ContinuousMapZero.id s) * a = 0) (hmul_star_id : φ (star (ContinuousMapZero.id s)) * a = 0) (hφ : Continuous ⇑φ) (f : ContinuousMapZero (↑s) 𝕜) : φ f * a = 0
• ContinuousMap.setOfIdeal_ofSet_eq_interior 📋 Mathlib.Topology.ContinuousMap.Ideals
  {X : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] (s : Set X) : ContinuousMap.setOfIdeal (ContinuousMap.idealOfSet 𝕜 s) = interior s
• ContinuousMap.setOfIdeal_ofSet_of_isOpen 📋 Mathlib.Topology.ContinuousMap.Ideals
  {X : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] {s : Set X} (hs : IsOpen s) : ContinuousMap.setOfIdeal (ContinuousMap.idealOfSet 𝕜 s) = s
• ContinuousMap.idealOf_compl_singleton_isMaximal 📋 Mathlib.Topology.ContinuousMap.Ideals
  {X : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] (x : X) : (ContinuousMap.idealOfSet 𝕜 {x}ᶜ).IsMaximal
• ContinuousMap.idealOfSet_isMaximal_iff 📋 Mathlib.Topology.ContinuousMap.Ideals
  {X : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] (s : TopologicalSpace.Opens X) : (ContinuousMap.idealOfSet 𝕜 ↑s).IsMaximal ↔ IsCoatom s
• ContinuousMap.setOfIdeal_eq_compl_singleton 📋 Mathlib.Topology.ContinuousMap.Ideals
  {X : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] (I : Ideal C(X, 𝕜)) [hI : I.IsMaximal] : ∃ x, ContinuousMap.setOfIdeal I = {x}ᶜ
• ContinuousMap.idealOfSet_ofIdeal_eq_closure 📋 Mathlib.Topology.ContinuousMap.Ideals
  {X : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] (I : Ideal C(X, 𝕜)) : ContinuousMap.idealOfSet 𝕜 (ContinuousMap.setOfIdeal I) = I.closure
• ContinuousMap.idealOpensGI 📋 Mathlib.Topology.ContinuousMap.Ideals
  (X : Type u_1) (𝕜 : Type u_2) [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] : GaloisInsertion ContinuousMap.opensOfIdeal fun s => ContinuousMap.idealOfSet 𝕜 ↑s
• ContinuousMap.idealOfSet_ofIdeal_isClosed 📋 Mathlib.Topology.ContinuousMap.Ideals
  {X : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] {I : Ideal C(X, 𝕜)} (hI : IsClosed ↑I) : ContinuousMap.idealOfSet 𝕜 (ContinuousMap.setOfIdeal I) = I
• ContinuousMap.ideal_isMaximal_iff 📋 Mathlib.Topology.ContinuousMap.Ideals
  {X : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] (I : Ideal C(X, 𝕜)) [hI : IsClosed ↑I] : I.IsMaximal ↔ ∃ x, ContinuousMap.idealOfSet 𝕜 {x}ᶜ = I
• ContinuousMap.idealOpensGI_choice 📋 Mathlib.Topology.ContinuousMap.Ideals
  (X : Type u_1) (𝕜 : Type u_2) [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] (I : Ideal C(X, 𝕜)) (x✝ : ContinuousMap.idealOfSet 𝕜 ↑(ContinuousMap.opensOfIdeal I) ≤ I) : (ContinuousMap.idealOpensGI X 𝕜).choice I x✝ = ContinuousMap.opensOfIdeal I.closure
• WeakDual.CharacterSpace.homeoEval 📋 Mathlib.Topology.ContinuousMap.Ideals
  (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [CompactSpace X] [T2Space X] [RCLike 𝕜] : X ≃ₜ ↑(WeakDual.characterSpace 𝕜 C(X, 𝕜))
• WeakDual.CharacterSpace.continuousMapEval_bijective 📋 Mathlib.Topology.ContinuousMap.Ideals
  (X : Type u_1) (𝕜 : Type u_2) [TopologicalSpace X] [CompactSpace X] [T2Space X] [RCLike 𝕜] : Function.Bijective ⇑(WeakDual.CharacterSpace.continuousMapEval X 𝕜)
• WeakDual.CharacterSpace.homeoEval_naturality 📋 Mathlib.Analysis.CStarAlgebra.GelfandDuality
  {X : Type u_1} {Y : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] [TopologicalSpace Y] [CompactSpace Y] [T2Space Y] (f : C(X, Y)) : (↑(WeakDual.CharacterSpace.homeoEval Y 𝕜)).comp f = (WeakDual.CharacterSpace.compContinuousMap (ContinuousMap.compStarAlgHom' 𝕜 𝕜 f)).comp ↑(WeakDual.CharacterSpace.homeoEval X 𝕜)
• IsCoveringMapOn.of_openPartialHomeomorph 📋 Mathlib.Topology.Covering.Basic
  {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {s : Set X} [T2Space E] [T2Space X] [CompactSpace E] (hf : Continuous f) (h : ∀ e ∈ f ⁻¹' s, ∃ φ, e ∈ φ.source ∧ ↑φ = f) : IsCoveringMapOn f s
• IsEvenlyCovered.of_openPartialHomeomorph 📋 Mathlib.Topology.Covering.Basic
  {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} [T2Space E] [T2Space X] [CompactSpace E] {x : X} (hf : Continuous f) (h : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f) : IsEvenlyCovered f x ↑(f ⁻¹' {x})
• continuous_ultrafilter_extend 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} {γ : Type u_1} [TopologicalSpace γ] [T2Space γ] [CompactSpace γ] (f : α → γ) : Continuous (Ultrafilter.extend f)
• preStoneCechExtend 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : α → β} (hg : Continuous g) : PreStoneCech α → β
• stoneCechExtend 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] {g : α → β} (hg : Continuous g) [CompactSpace β] : StoneCech α → β
• continuous_preStoneCechExtend 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : α → β} (hg : Continuous g) : Continuous (preStoneCechExtend hg)
• continuous_stoneCechExtend 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] {g : α → β} (hg : Continuous g) [CompactSpace β] : Continuous (stoneCechExtend hg)
• preStoneCechExtend_preStoneCechUnit 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : α → β} (hg : Continuous g) (a : α) : preStoneCechExtend hg (preStoneCechUnit a) = g a
• stoneCechExtend_stoneCechUnit 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] {g : α → β} (hg : Continuous g) [CompactSpace β] (a : α) : stoneCechExtend hg (stoneCechUnit a) = g a
• eq_if_preStoneCechUnit_eq 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : α → β} (hg : Continuous g) {a b : α} (h : preStoneCechUnit a = preStoneCechUnit b) : g a = g b
• eq_if_stoneCechUnit_eq 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {a b : α} {f : α → β} (hcf : Continuous f) (h : stoneCechUnit a = stoneCechUnit b) : f a = f b
• preStoneCechExtend_extends 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : α → β} (hg : Continuous g) : preStoneCechExtend hg ∘ preStoneCechUnit = g
• stoneCechExtend_extends 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] {g : α → β} (hg : Continuous g) [CompactSpace β] : stoneCechExtend hg ∘ stoneCechUnit = g
• ultrafilter_extend_eq_iff 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} {γ : Type u_1} [TopologicalSpace γ] [T2Space γ] [CompactSpace γ] {f : α → γ} {b : Ultrafilter α} {c : γ} : Ultrafilter.extend f b = c ↔ ↑(Ultrafilter.map f b) ≤ nhds c
• preStoneCechCompat 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : α → β} (hg : Continuous g) {F G : Ultrafilter α} {x : α} (hF : ↑F ≤ nhds x) (hG : ↑G ≤ nhds x) : Ultrafilter.extend g F = Ultrafilter.extend g G
• CompHausLike.mk 📋 Mathlib.Topology.Category.CompHausLike.Basic
  {P : TopCat → Prop} (toTop : TopCat) [is_compact : CompactSpace ↑toTop] [is_hausdorff : T2Space ↑toTop] (prop : P toTop) : CompHausLike P
• CompHausLike.of 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) (X : Type u) [TopologicalSpace X] [CompactSpace X] [T2Space X] [CompHausLike.HasProp P X] : CompHausLike P
• CompHausLike.coe_of 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) (X : Type u) [TopologicalSpace X] [CompactSpace X] [T2Space X] [CompHausLike.HasProp P X] : ↑(CompHausLike.of P X).toTop = X
• CompHausLike.ofHom 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) {X : Type u} [TopologicalSpace X] [CompactSpace X] [T2Space X] [CompHausLike.HasProp P X] {Y : Type u} [TopologicalSpace Y] [CompactSpace Y] [T2Space Y] [CompHausLike.HasProp P Y] (f : C(X, Y)) : CompHausLike.of P X ⟶ CompHausLike.of P Y
• CompHausLike.ofHom_id 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) {X : Type u} [TopologicalSpace X] [CompactSpace X] [T2Space X] [CompHausLike.HasProp P X] : CompHausLike.ofHom P (ContinuousMap.id X) = CategoryTheory.CategoryStruct.id (CompHausLike.of P X)
• CompHausLike.ofHom_comp 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) {X : Type u} [TopologicalSpace X] [CompactSpace X] [T2Space X] [CompHausLike.HasProp P X] {Y : Type u} [TopologicalSpace Y] [CompactSpace Y] [T2Space Y] [CompHausLike.HasProp P Y] {Z : Type u} [TopologicalSpace Z] [CompactSpace Z] [T2Space Z] [CompHausLike.HasProp P Z] (f : C(X, Y)) (g : C(Y, Z)) : CompHausLike.ofHom P (g.comp f) = CategoryTheory.CategoryStruct.comp (CompHausLike.ofHom P f) (CompHausLike.ofHom P g)
• CompHausLike.hom_ofHom 📋 Mathlib.Topology.Category.CompHausLike.Basic
  (P : TopCat → Prop) {X : Type u} [TopologicalSpace X] [CompactSpace X] [T2Space X] [CompHausLike.HasProp P X] {Y : Type u} [TopologicalSpace Y] [CompactSpace Y] [T2Space Y] [CompHausLike.HasProp P Y] (f : C(X, Y)) : CategoryTheory.ConcreteCategory.hom (CompHausLike.ofHom P f) = f
• CompHaus.of 📋 Mathlib.Topology.Category.CompHaus.Basic
  (X : Type u_1) [TopologicalSpace X] [CompactSpace X] [T2Space X] : CompHaus
• OnePoint.equivOfIsEmbeddingOfRangeEq 📋 Mathlib.Topology.Compactification.OnePoint.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] (y : Y) (f : X → Y) (hf : Topology.IsEmbedding f) (hy : Set.range f = {y}ᶜ) : OnePoint X ≃ₜ Y
• OnePoint.equivOfIsEmbeddingOfRangeEq_apply_infty 📋 Mathlib.Topology.Compactification.OnePoint.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] (y : Y) (f : X → Y) (hf : Topology.IsEmbedding f) (hy : Set.range f = {y}ᶜ) : (OnePoint.equivOfIsEmbeddingOfRangeEq y f hf hy) OnePoint.infty = y
• OnePoint.equivOfIsEmbeddingOfRangeEq_apply_coe 📋 Mathlib.Topology.Compactification.OnePoint.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] (y : Y) (f : X → Y) (hf : Topology.IsEmbedding f) (hy : Set.range f = {y}ᶜ) (x : X) : (OnePoint.equivOfIsEmbeddingOfRangeEq y f hf hy) ↑x = f x
• compactlyGeneratedSpace_of_isClosed 📋 Mathlib.Topology.Compactness.CompactlyGeneratedSpace
  {X : Type u} [TopologicalSpace X] (h : ∀ (s : Set X), (∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X), Continuous f → IsClosed (f ⁻¹' s)) → IsClosed s) : CompactlyGeneratedSpace X
• compactlyGeneratedSpace_of_isOpen 📋 Mathlib.Topology.Compactness.CompactlyGeneratedSpace
  {X : Type u} [TopologicalSpace X] (h : ∀ (s : Set X), (∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X), Continuous f → IsOpen (f ⁻¹' s)) → IsOpen s) : CompactlyGeneratedSpace X
• CompactlyGeneratedSpace.isClosed' 📋 Mathlib.Topology.Compactness.CompactlyGeneratedSpace
  {X : Type u} [TopologicalSpace X] [CompactlyGeneratedSpace X] {s : Set X} (hs : ∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X), Continuous f → IsClosed (f ⁻¹' s)) : IsClosed s
• CompactlyGeneratedSpace.isOpen' 📋 Mathlib.Topology.Compactness.CompactlyGeneratedSpace
  {X : Type u} [TopologicalSpace X] [CompactlyGeneratedSpace X] {s : Set X} (hs : ∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X), Continuous f → IsOpen (f ⁻¹' s)) : IsOpen s
• compactlyGeneratedSpace_of_continuous_maps 📋 Mathlib.Topology.Compactness.CompactlyGeneratedSpace
  {X : Type u} [TopologicalSpace X] (h : ∀ {Y : Type u} [inst : TopologicalSpace Y] (f : X → Y), (∀ (K : Type u) [inst_1 : TopologicalSpace K] [CompactSpace K] [T2Space K] (g : K → X), Continuous g → Continuous (f ∘ g)) → Continuous f) : CompactlyGeneratedSpace X
• continuous_from_compactlyGeneratedSpace 📋 Mathlib.Topology.Compactness.CompactlyGeneratedSpace
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [CompactlyGeneratedSpace X] (f : X → Y) (h : ∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (g : K → X), Continuous g → Continuous (f ∘ g)) : Continuous f
• 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_const_add : ∀ (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_const_mul : ∀ (r : M), Continuous fun x => x * r) : ∃ m, m * m = m
• isTopologicalBasis_isClopen 📋 Mathlib.Topology.Separation.Profinite
  {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [TotallyDisconnectedSpace X] : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
• nhds_basis_clopen 📋 Mathlib.Topology.Separation.Profinite
  {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [TotallyDisconnectedSpace X] (x : X) : (nhds x).HasBasis (fun s => x ∈ s ∧ IsClopen s) id
• compact_exists_isClopen_in_isOpen 📋 Mathlib.Topology.Separation.Profinite
  {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [TotallyDisconnectedSpace X] {x : X} {U : Set X} (is_open : IsOpen U) (memU : x ∈ U) : ∃ V, IsClopen V ∧ x ∈ V ∧ V ⊆ U
• exists_clopen_of_closed_subset_open 📋 Mathlib.Topology.Separation.Profinite
  {X : Type u_4} [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] {Z U : Set X} (hZ : IsClosed Z) (hU : IsOpen U) (hZU : Z ⊆ U) : ∃ C, IsClopen C ∧ Z ⊆ C ∧ C ⊆ U
• exists_clopen_partition_of_clopen_cover 📋 Mathlib.Topology.Separation.Profinite
  {X : Type u_4} {I : Type u_5} [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] [Finite I] {Z D : I → Set X} (Z_closed : ∀ (i : I), IsClosed (Z i)) (D_clopen : ∀ (i : I), IsClopen (D i)) (Z_subset_D : ∀ (i : I), Z i ⊆ D i) (Z_disj : Set.univ.PairwiseDisjoint Z) : ∃ C, (∀ (i : I), IsClopen (C i)) ∧ (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ Set.univ.PairwiseDisjoint C
• Profinite.of 📋 Mathlib.Topology.Category.Profinite.Basic
  (X : Type u_1) [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] : Profinite
• CompactT2.ExtremallyDisconnected.projective 📋 Mathlib.Topology.ExtremallyDisconnected
  {A : Type u} [TopologicalSpace A] [ExtremallyDisconnected A] [CompactSpace A] [T2Space A] : CompactT2.Projective A
• CompactT2.Projective.extremallyDisconnected 📋 Mathlib.Topology.ExtremallyDisconnected
  {X : Type u} [TopologicalSpace X] [CompactSpace X] [T2Space X] (h : CompactT2.Projective X) : ExtremallyDisconnected X
• CompactT2.projective_iff_extremallyDisconnected 📋 Mathlib.Topology.ExtremallyDisconnected
  {A : Type u} [TopologicalSpace A] [CompactSpace A] [T2Space A] : CompactT2.Projective A ↔ ExtremallyDisconnected A
• ExtremallyDisconnected.homeoCompactToT2 📋 Mathlib.Topology.ExtremallyDisconnected
  {A E : Type u} [TopologicalSpace A] [TopologicalSpace E] [ExtremallyDisconnected A] [T2Space A] [T2Space E] [CompactSpace E] {ρ : E → A} (ρ_cont : Continuous ρ) (ρ_surj : Function.Surjective ρ) (zorn_subset : ∀ (E₀ : Set E), E₀ ≠ Set.univ → IsClosed E₀ → ρ '' E₀ ≠ Set.univ) : E ≃ₜ A
• Stonean.of 📋 Mathlib.Topology.Category.Stonean.Basic
  (X : Type u_1) [TopologicalSpace X] [CompactSpace X] [T2Space X] [ExtremallyDisconnected X] : Stonean
• DiscreteQuotient.eq_of_forall_proj_eq 📋 Mathlib.Topology.DiscreteQuotient
  {X : Type u_2} [TopologicalSpace X] [T2Space X] [CompactSpace X] [disc : TotallyDisconnectedSpace X] {x y : X} (h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y) : x = y
• TopologicalSpace.Clopens.countable_iff_secondCountable 📋 Mathlib.Topology.ClopenBox
  {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] : Countable (TopologicalSpace.Clopens X) ↔ SecondCountableTopology X
• LightProfinite.of 📋 Mathlib.Topology.Category.LightProfinite.Basic
  (X : Type u_1) [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] [SecondCountableTopology X] : LightProfinite
• CompHausLike.instHasPropSigma 📋 Mathlib.Topology.Category.CompHausLike.SigmaComparison
  {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] {α : Type u} [Finite α] (σ : α → Type u) [(a : α) → TopologicalSpace (σ a)] [∀ (a : α), CompactSpace (σ a)] [∀ (a : α), T2Space (σ a)] [∀ (a : α), CompHausLike.HasProp P (σ a)] : CompHausLike.HasProp P ((a : α) × σ a)
• CompHausLike.sigmaComparison 📋 Mathlib.Topology.Category.CompHausLike.SigmaComparison
  {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) {α : Type u} [Finite α] (σ : α → Type u) [(a : α) → TopologicalSpace (σ a)] [∀ (a : α), CompactSpace (σ a)] [∀ (a : α), T2Space (σ a)] [∀ (a : α), CompHausLike.HasProp P (σ a)] : X.obj (Opposite.op (CompHausLike.of P ((a : α) × σ a))) ⟶ (a : α) → X.obj (Opposite.op (CompHausLike.of P (σ a)))
• CompHausLike.isIsoSigmaComparison 📋 Mathlib.Topology.Category.CompHausLike.SigmaComparison
  {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) [CategoryTheory.Limits.PreservesFiniteProducts X] {α : Type u} [Finite α] (σ : α → Type u) [(a : α) → TopologicalSpace (σ a)] [∀ (a : α), CompactSpace (σ a)] [∀ (a : α), T2Space (σ a)] [∀ (a : α), CompHausLike.HasProp P (σ a)] : CategoryTheory.IsIso (CompHausLike.sigmaComparison X σ)
• CompHausLike.sigmaComparison_eq_comp_isos 📋 Mathlib.Topology.Category.CompHausLike.SigmaComparison
  {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) [CategoryTheory.Limits.PreservesFiniteProducts X] {α : Type u} [Finite α] (σ : α → Type u) [(a : α) → TopologicalSpace (σ a)] [∀ (a : α), CompactSpace (σ a)] [∀ (a : α), T2Space (σ a)] [∀ (a : α), CompHausLike.HasProp P (σ a)] : CompHausLike.sigmaComparison X σ = CategoryTheory.CategoryStruct.comp (X.mapIso (CategoryTheory.Limits.opCoproductIsoProduct' (CompHausLike.finiteCoproduct.isColimit fun a => CompHausLike.of P (σ a)) (CategoryTheory.Limits.productIsProduct fun x => Opposite.op (CompHausLike.of P (σ x))))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesProduct.iso X fun a => Opposite.op (CompHausLike.of P (σ a))).hom (CategoryTheory.Limits.Types.productIso fun a => X.obj (Opposite.op (CompHausLike.of P (σ a)))).hom)
• 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% e x)
• MeasureTheory.Measure.exists_regular_eq_of_compactSpace 📋 Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
  {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] : ∃ ν, ν.Regular ∧ MeasureTheory.IsFiniteMeasure ν ∧ ∀ (g : BoundedContinuousFunction X ℝ), ∫ (x : X), g x ∂μ = ∫ (x : X), g x ∂ν
• RealRMK.instIsFiniteMeasureRieszMeasure 📋 Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
  {X : Type u_1} [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) : MeasureTheory.IsFiniteMeasure (RealRMK.rieszMeasure Λ)
• instCompactSpaceProbabilityMeasure 📋 Mathlib.MeasureTheory.Measure.Prokhorov
  {E : Type u_1} [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] [CompactSpace E] : CompactSpace (MeasureTheory.ProbabilityMeasure E)
• isCompact_setOf_finiteMeasure_eq_of_compactSpace 📋 Mathlib.MeasureTheory.Measure.Prokhorov
  (E : Type u_1) [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] [CompactSpace E] (C : NNReal) : IsCompact {μ | μ.mass = C}
• isCompact_setOf_finiteMeasure_le_of_compactSpace 📋 Mathlib.MeasureTheory.Measure.Prokhorov
  (E : Type u_1) [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E] [CompactSpace E] (C : NNReal) : IsCompact {μ | μ.mass ≤ C}
• ContinuousAddMonoidHom.instCompactSpace 📋 Mathlib.Topology.Algebra.Group.CompactOpen
  {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [DiscreteTopology A] [ContinuousAdd B] [T2Space B] [CompactSpace B] : CompactSpace (A →ₜ+ B)
• ContinuousMonoidHom.instCompactSpace 📋 Mathlib.Topology.Algebra.Group.CompactOpen
  {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [DiscreteTopology A] [ContinuousMul B] [T2Space B] [CompactSpace B] : CompactSpace (A →ₜ* B)
• IsNoetherianRing.isClosed_ideal 📋 Mathlib.Topology.Algebra.Module.Compact
  {R : Type u_3} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [IsNoetherianRing R] [CompactSpace R] [T2Space R] (I : Ideal R) : IsClosed ↑I
• instProperConstSMulOfContinuousConstSMulOfT2SpaceOfCompactSpace 📋 Mathlib.Topology.Algebra.ProperConstSMul
  {M : Type u_1} {X : Type u_2} [SMul M X] [TopologicalSpace X] [ContinuousConstSMul M X] [T2Space X] [CompactSpace X] : ProperConstSMul M X
• instProperConstVAddOfContinuousConstVAddOfT2SpaceOfCompactSpace 📋 Mathlib.Topology.Algebra.ProperConstSMul
  {M : Type u_1} {X : Type u_2} [VAdd M X] [TopologicalSpace X] [ContinuousConstVAdd M X] [T2Space X] [CompactSpace X] : ProperConstVAdd M X
• 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)
• instFiniteQuotientIdealOfIsMaximal 📋 Mathlib.Topology.Algebra.Ring.Compact
  {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsNoetherianRing R] (I : Ideal R) [I.IsMaximal] : Finite (R ⧸ I)
• IsLocalRing.isOpen_maximalIdeal 📋 Mathlib.Topology.Algebra.Ring.Compact
  (R : Type u_1) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsLocalRing R] [IsNoetherianRing R] : IsOpen ↑(IsLocalRing.maximalIdeal R)
• Ideal.isOpen_of_isMaximal 📋 Mathlib.Topology.Algebra.Ring.Compact
  {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsNoetherianRing R] (I : Ideal R) [I.IsMaximal] : IsOpen ↑I
• IsLocalRing.isOpen_iff_finite_quotient 📋 Mathlib.Topology.Algebra.Ring.Compact
  {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsLocalRing R] [IsNoetherianRing R] {I : Ideal R} : IsOpen ↑I ↔ Finite (R ⧸ I)
• IsDedekindDomain.isOpen_of_ne_bot 📋 Mathlib.Topology.Algebra.Ring.Compact
  {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ ⊥) : IsOpen ↑I
• IsDedekindDomain.isOpen_iff 📋 Mathlib.Topology.Algebra.Ring.Compact
  {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsDedekindDomain R] (hR : ¬IsField R) {I : Ideal R} : IsOpen ↑I ↔ I ≠ ⊥
• IsDiscreteValuationRing.isOpen_iff 📋 Mathlib.Topology.Algebra.Ring.Compact
  {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsDomain R] [IsDiscreteValuationRing R] {I : Ideal R} : IsOpen ↑I ↔ I ≠ ⊥
• IsLocalRing.isOpen_maximalIdeal_pow 📋 Mathlib.Topology.Algebra.Ring.Compact
  (R : Type u_1) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsLocalRing R] [IsNoetherianRing R] (n : ℕ) : IsOpen ↑(IsLocalRing.maximalIdeal R ^ n)
• Ideal.isOpen_pow_of_isMaximal 📋 Mathlib.Topology.Algebra.Ring.Compact
  {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsNoetherianRing R] (I : Ideal R) [I.IsMaximal] (n : ℕ) : IsOpen ↑(I ^ n)
• Compactum.ofTopologicalSpace 📋 Mathlib.Topology.Category.Compactum
  (X : Type u_1) [TopologicalSpace X] [CompactSpace X] [T2Space X] : Compactum
• Profinite.exists_lift_of_finite_of_injective_of_surjective 📋 Mathlib.Topology.Category.LightProfinite.Injective
  {X : Type u_1} {Y : Type u_2} {S : Type u_3} {T : Type u_4} [TopologicalSpace X] [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [T2Space Y] [TotallyDisconnectedSpace Y] [TopologicalSpace S] [T2Space S] [Finite S] [TopologicalSpace T] [T2Space T] (f : X → Y) (hf : Continuous f) (f_inj : Function.Injective f) (f' : S → T) (f'_surj : Function.Surjective f') (g : X → S) (hg : Continuous g) (g' : Y → T) (hg' : Continuous g') (h_comm : g' ∘ f = f' ∘ g) : ∃ k, Continuous k ∧ f' ∘ k = g' ∧ k ∘ f = g
• BoundedContinuousFunction.arzela_ascoli 📋 Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
  {α : Type u} {β : Type v} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] [T2Space β] (s : Set β) (hs : IsCompact s) (A : Set (BoundedContinuousFunction α β)) (in_s : ∀ (f : BoundedContinuousFunction α β) (x : α), f ∈ A → f x ∈ s) (H : Equicontinuous fun x => ⇑↑x) : IsCompact (closure A)
• TopologicalSpace.IsOpenCover.exists_finite_clopen_cover 📋 Mathlib.Topology.Separation.DisjointCover
  {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] {U : ι → TopologicalSpace.Opens X} (hU : TopologicalSpace.IsOpenCover U) : ∃ n V, (∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)) ∧ Set.univ ⊆ ⋃ j, ↑(V j)
• ContinuousMap.exists_finite_approximation_of_mem_nhds_diagonal 📋 Mathlib.Topology.Separation.DisjointCover
  {X : Type u_1} {V : Type u_2} [TopologicalSpace X] [TopologicalSpace V] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] {S : Set (V × V)} (f : C(X, V)) (hS : S ∈ nhdsSet (Set.diagonal V)) : ∃ n g h, Continuous g ∧ ∀ (x : X), (f x, h (g x)) ∈ S
• TopologicalSpace.IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover 📋 Mathlib.Topology.Separation.DisjointCover
  {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] {U : ι → TopologicalSpace.Opens X} (hU : TopologicalSpace.IsOpenCover U) : ∃ n W, (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ i, ↑(W j) ⊆ ↑(U i)) ∧ Set.univ ⊆ ⋃ j, ↑(W j) ∧ Pairwise (Function.onFun Disjoint W)
• ContinuousMap.exists_finite_sum_const_indicator_approximation_of_mem_nhds_diagonal 📋 Mathlib.Topology.Separation.DisjointCover
  {X : Type u_1} {V : Type u_2} [TopologicalSpace X] [TopologicalSpace V] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] {S : Set (V × V)} (f : C(X, V)) [AddCommMonoid V] (hS : S ∈ nhdsSet (Set.diagonal V)) : ∃ n U v, ∀ (x : X), (f x, ∑ n, (↑(U n)).indicator (fun x => v n) x) ∈ S
• ContinuousMap.exists_finite_sum_const_mulIndicator_approximation_of_mem_nhds_diagonal 📋 Mathlib.Topology.Separation.DisjointCover
  {X : Type u_1} {V : Type u_2} [TopologicalSpace X] [TopologicalSpace V] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] {S : Set (V × V)} (f : C(X, V)) [CommMonoid V] (hS : S ∈ nhdsSet (Set.diagonal V)) : ∃ n U v, ∀ (x : X), (f x, ∏ n, (↑(U n)).mulIndicator (fun x => v n) x) ∈ S
• ContinuousMap.exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal 📋 Mathlib.Topology.Separation.DisjointCover
  {X : Type u_1} {V : Type u_2} [TopologicalSpace X] [TopologicalSpace V] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] {S : Set (V × V)} (f : C(X, V)) (hS : S ∈ nhdsSet (Set.diagonal V)) : ∃ n D, (∀ (i : Fin n), D i ≠ ⊥) ∧ (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (f y, f z) ∈ S) ∧ Set.univ ⊆ ⋃ i, ↑(D i) ∧ Pairwise (Function.onFun Disjoint D)
• ContinuousMap.exists_finite_sum_mul_approximation_of_mem_uniformity 📋 Mathlib.Topology.UniformSpace.ProdApproximation
  {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [Ring R] [UniformSpace R] [IsUniformAddGroup R] (f : C(X × Y, R)) {S : Set (R × R)} (hS : S ∈ uniformity R) : ∃ n g h, ∀ (x : X) (y : Y), (f (x, y), ∑ i, (g i) x * (h i) y) ∈ S
• ContinuousMap.exists_finite_sum_smul_approximation_of_mem_uniformity 📋 Mathlib.Topology.UniformSpace.ProdApproximation
  {X : Type u_1} {Y : Type u_2} {R : Type u_3} {V : Type u_4} [TopologicalSpace X] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] [TopologicalSpace Y] [CompactSpace Y] [AddCommGroup V] [UniformSpace V] [IsUniformAddGroup V] {S : Set (V × V)} [TopologicalSpace R] [MonoidWithZero R] [MulActionWithZero R V] (f : C(X × Y, V)) (hS : S ∈ uniformity V) : ∃ n g h, ∀ (x : X) (y : Y), (f (x, y), ∑ i, (g i) x • (h i) y) ∈ 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.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 8e80836 serving mathlib revision 6ef8cc2