Loogle!

Result

Found 1073 declarations mentioning IsCompact. Of these, only the first 200 are shown.

• IsCompact 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_1} [TopologicalSpace X] (s : Set X) : Prop
• CompactSpace.isCompact_univ 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_1} {inst✝ : TopologicalSpace X} [self : CompactSpace X] : IsCompact Set.univ
• CompactSpace.mk 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_1} [TopologicalSpace X] (isCompact_univ : IsCompact Set.univ) : CompactSpace X
• NoncompactSpace.mk 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_1} [TopologicalSpace X] (noncompact_univ : ¬IsCompact Set.univ) : NoncompactSpace X
• NoncompactSpace.noncompact_univ 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_1} {inst✝ : TopologicalSpace X} [self : NoncompactSpace X] : ¬IsCompact Set.univ
• WeaklyLocallyCompactSpace.exists_compact_mem_nhds 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_3} {inst✝ : TopologicalSpace X} [self : WeaklyLocallyCompactSpace X] (x : X) : ∃ s, IsCompact s ∧ s ∈ nhds x
• WeaklyLocallyCompactSpace.mk 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_3} [TopologicalSpace X] (exists_compact_mem_nhds : ∀ (x : X), ∃ s, IsCompact s ∧ s ∈ nhds x) : WeaklyLocallyCompactSpace X
• LocallyCompactSpace.local_compact_nhds 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_3} {inst✝ : TopologicalSpace X} [self : LocallyCompactSpace X] (x : X) (n : Set X) : n ∈ nhds x → ∃ s ∈ nhds x, s ⊆ n ∧ IsCompact s
• LocallyCompactSpace.mk 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_3} [TopologicalSpace X] (local_compact_nhds : ∀ (x : X), ∀ n ∈ nhds x, ∃ s ∈ nhds x, s ⊆ n ∧ IsCompact s) : LocallyCompactSpace X
• LocallyCompactPair.exists_mem_nhds_isCompact_mapsTo 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_3} {Y : Type u_4} {inst✝ : TopologicalSpace X} {inst✝¹ : TopologicalSpace Y} [self : LocallyCompactPair X Y] {f : X → Y} {x : X} {s : Set Y} : Continuous f → s ∈ nhds (f x) → ∃ K ∈ nhds x, IsCompact K ∧ Set.MapsTo f K s
• LocallyCompactPair.mk 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] (exists_mem_nhds_isCompact_mapsTo : ∀ {f : X → Y} {x : X} {s : Set Y}, Continuous f → s ∈ nhds (f x) → ∃ K ∈ nhds x, IsCompact K ∧ Set.MapsTo f K s) : LocallyCompactPair X Y
• isCompact_empty 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] : IsCompact ∅
• isCompact_univ 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] [h : CompactSpace X] : IsCompact Set.univ
• isCompact_univ_iff 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] : IsCompact Set.univ ↔ CompactSpace X
• noncompact_univ 📋 Mathlib.Topology.Compactness.Compact
  (X : Type u_2) [TopologicalSpace X] [NoncompactSpace X] : ¬IsCompact Set.univ
• Set.Finite.isCompact 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : s.Finite) : IsCompact s
• Set.Subsingleton.isCompact 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : s.Subsingleton) : IsCompact s
• isCompact_singleton 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {x : X} : IsCompact {x}
• IsCompact.finite_of_discrete 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} [DiscreteTopology X] (hs : IsCompact s) : s.Finite
• isCompact_iff_finite 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} [DiscreteTopology X] : IsCompact s ↔ s.Finite
• IsClosed.isCompact 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} [CompactSpace X] (h : IsClosed s) : IsCompact s
• IsCompact.finite 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (hs' : IsDiscrete s) : s.Finite
• isCompact_diagonal 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] [CompactSpace X] : IsCompact (Set.diagonal X)
• Filter.hasBasis_cocompact 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] : (Filter.cocompact X).HasBasis IsCompact compl
• IsCompact.ne_univ 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} [NoncompactSpace X] (hs : IsCompact s) : s ≠ Set.univ
• IsCompact.insert 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (a : X) : IsCompact (insert a s)
• isCompact_accumulate 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {K : ℕ → Set X} (hK : ∀ (n : ℕ), IsCompact (K n)) (n : ℕ) : IsCompact (Set.accumulate K n)
• isCompact_iUnion 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {ι : Sort u_2} {f : ι → Set X} [Finite ι] (h : ∀ (i : ι), IsCompact (f i)) : IsCompact (⋃ i, f i)
• isCompact_range 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] {f : X → Y} (hf : Continuous f) : IsCompact (Set.range f)
• IsCompact.compl_mem_cocompact 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) : sᶜ ∈ Filter.cocompact X
• IsCompact.diff 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsCompact s) (ht : IsOpen t) : IsCompact (s \ t)
• IsCompact.inter_left 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s t : Set X} (ht : IsCompact t) (hs : IsClosed s) : IsCompact (s ∩ t)
• IsCompact.inter_right 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsCompact s) (ht : IsClosed t) : IsCompact (s ∩ t)
• IsCompact.union 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ∪ t)
• isCompact_iff_compactSpace 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsCompact s ↔ CompactSpace ↑s
• Filter.hasBasis_coclosedCompact 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] : (Filter.coclosedCompact X).HasBasis (fun s => IsClosed s ∧ IsCompact s) compl
• IsCompact.of_isClosed_subset 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsCompact s) (ht : IsClosed t) (h : t ⊆ s) : IsCompact t
• Set.sUnion_isCompact_eq_univ 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] : ⋃₀ {s | IsCompact s} = Set.univ
• IsCompact.image 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hs : IsCompact s) (hf : Continuous f) : IsCompact (f '' s)
• Topology.IsClosedEmbedding.isCompact_preimage 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsClosedEmbedding f) {K : Set Y} (hK : IsCompact K) : IsCompact (f ⁻¹' K)
• Filter.compl_mem_coclosedCompact 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} : sᶜ ∈ Filter.coclosedCompact X ↔ IsCompact (closure s)
• Filter.mem_coclosedCompact_iff 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} : s ∈ Filter.coclosedCompact X ↔ IsCompact (closure sᶜ)
• IsCompact.compl_mem_coclosedCompact_of_isClosed 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (hs' : IsClosed s) : sᶜ ∈ Filter.coclosedCompact X
• IsCompact.image_of_continuousOn 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hs : IsCompact s) (hf : ContinuousOn f s) : IsCompact (f '' s)
• Bornology.inCompact.isBounded_iff 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} : Bornology.IsBounded s ↔ ∃ t, IsCompact t ∧ s ⊆ t
• Topology.IsEmbedding.isCompact_iff 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf : Topology.IsEmbedding f) : IsCompact s ↔ IsCompact (f '' s)
• Topology.IsInducing.isCompact_iff 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf : Topology.IsInducing f) : IsCompact s ↔ IsCompact (f '' s)
• isCompact_iff_isCompact_univ 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsCompact s ↔ IsCompact Set.univ
• Filter.Tendsto.isCompact_insert_range 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {f : ℕ → X} {x : X} (hf : Filter.Tendsto f Filter.atTop (nhds x)) : IsCompact (insert x (Set.range f))
• Filter.Tendsto.isCompact_insert_range_of_cofinite 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {ι : Type u_1} [TopologicalSpace X] {f : ι → X} {x : X} (hf : Filter.Tendsto f Filter.cofinite (nhds x)) : IsCompact (insert x (Set.range f))
• isCompact_univ_pi 📋 Mathlib.Topology.Compactness.Compact
  {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {s : (i : ι) → Set (X i)} (h : ∀ (i : ι), IsCompact (s i)) : IsCompact (Set.univ.pi s)
• Set.Finite.isCompact_sUnion 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {S : Set (Set X)} (hf : S.Finite) (hc : ∀ s ∈ S, IsCompact s) : IsCompact (⋃₀ S)
• Topology.IsInducing.isCompact_preimage 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsInducing f) (hf' : IsClosed (Set.range f)) {K : Set Y} (hK : IsCompact K) : IsCompact (f ⁻¹' K)
• Topology.IsInducing.isCompact_preimage' 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsInducing f) {K : Set Y} (hK : IsCompact K) (Kf : K ⊆ Set.range f) : IsCompact (f ⁻¹' K)
• Filter.mem_cocompact 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} : s ∈ Filter.cocompact X ↔ ∃ t, IsCompact t ∧ tᶜ ⊆ s
• Filter.mem_cocompact' 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} : s ∈ Filter.cocompact X ↔ ∃ t, IsCompact t ∧ sᶜ ⊆ t
• Topology.IsInducing.isCompact_preimage_iff 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsInducing f) {K : Set Y} (Kf : K ⊆ Set.range f) : IsCompact (f ⁻¹' K) ↔ IsCompact K
• IsCompact.exists_clusterPt_of_frequently 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} {l : Filter X} (hs : IsCompact s) (hl : ∃ᶠ (x : X) in l, x ∈ s) : ∃ a ∈ s, ClusterPt a l
• Filter.Tendsto.isCompact_insert_range_of_cocompact 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {y : Y} (hf : Filter.Tendsto f (Filter.cocompact X) (nhds y)) (hfc : Continuous f) : IsCompact (insert y (Set.range f))
• Set.Infinite.exists_accPt_of_subset_isCompact 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s K : Set X} (hs : s.Infinite) (hK : IsCompact K) (hsub : s ⊆ K) : ∃ x ∈ K, AccPt x (Filter.principal s)
• IsCompact.prod 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ×ˢ t)
• Subtype.isCompact_iff 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {p : X → Prop} {s : Set { x // p x }} : IsCompact s ↔ IsCompact (Subtype.val '' s)
• IsCompact.exists_clusterPt 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {f : Filter X} [f.NeBot] (hf : f ≤ Filter.principal s) : ∃ x ∈ s, ClusterPt x f
• IsCompact.exists_mapClusterPt_of_frequently 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {ι : Type u_1} [TopologicalSpace X] {s : Set X} {l : Filter ι} {f : ι → X} (hs : IsCompact s) (hf : ∃ᶠ (x : ι) in l, f x ∈ s) : ∃ a ∈ s, MapClusterPt a l f
• Pi.isCompact_iff_of_isClosed 📋 Mathlib.Topology.Compactness.Compact
  {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {s : Set ((i : ι) → X i)} (hs : IsClosed s) : IsCompact s ↔ ∀ (i : ι), IsCompact (Function.eval i '' s)
• Set.Infinite.exists_accPt_cofinite_inf_principal_of_subset_isCompact 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s K : Set X} (hs : s.Infinite) (hK : IsCompact K) (hsub : s ⊆ K) : ∃ x ∈ K, AccPt x (Filter.cofinite ⊓ Filter.principal s)
• isCompact_pi_infinite 📋 Mathlib.Topology.Compactness.Compact
  {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {s : (i : ι) → Set (X i)} : (∀ (i : ι), IsCompact (s i)) → IsCompact {x | ∀ (i : ι), x i ∈ s i}
• Bornology.isBounded_image_of_isLocallyBounded_of_isCompact 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {Y : Type u_2} [Bornology Y] {s : Set X} (hs : IsCompact s) {f : X → Y} (hf : ∀ (x : X), ∃ t ∈ nhds x, Bornology.IsBounded (f '' t)) : Bornology.IsBounded (f '' s)
• Set.isCompact_sigma 📋 Mathlib.Topology.Compactness.Compact
  {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {s : Set ι} {t : (i : ι) → Set (X i)} (hs : s.Finite) (ht : ∀ i ∈ s, IsCompact (t i)) : IsCompact (s.sigma t)
• exists_nhds_ne_inf_principal_neBot 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (hs' : s.Infinite) : ∃ z ∈ s, (nhdsWithin z {z}ᶜ ⊓ Filter.principal s).NeBot
• Filter.disjoint_cocompact_left 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] (f : Filter X) : Disjoint (Filter.cocompact X) f ↔ ∃ K ∈ f, IsCompact K
• Filter.disjoint_cocompact_right 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] (f : Filter X) : Disjoint f (Filter.cocompact X) ↔ ∃ K ∈ f, IsCompact K
• IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {ι : Type v} [hι : Nonempty ι] (t : ι → Set X) (htd : Directed (fun x1 x2 => x1 ⊇ x2) t) (htn : ∀ (i : ι), (t i).Nonempty) (htc : ∀ (i : ι), IsCompact (t i)) (htcl : ∀ (i : ι), IsClosed (t i)) : (⋂ i, t i).Nonempty
• IsCompact.ultrafilter_le_nhds' 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsCompact s → ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ nhds x
• isCompact_iff_ultrafilter_le_nhds' 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsCompact s ↔ ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ nhds x
• Set.Finite.isCompact_biUnion 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {ι : Type u_1} [TopologicalSpace X] {s : Set ι} {f : ι → Set X} (hs : s.Finite) (hf : ∀ i ∈ s, IsCompact (f i)) : IsCompact (⋃ i ∈ s, f i)
• IsCompact.exists_mapClusterPt 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} {ι : Type u_2} (hs : IsCompact s) {f : Filter ι} [f.NeBot] {u : ι → X} (hf : Filter.map u f ≤ Filter.principal s) : ∃ x ∈ s, MapClusterPt x f u
• IsCompact.le_nhds_of_unique_clusterPt 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {l : Filter X} {y : X} (hmem : s ∈ l) (h : ∀ x ∈ s, ClusterPt x l → x = y) : l ≤ nhds y
• IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] (t : ℕ → Set X) (htd : ∀ (i : ℕ), t (i + 1) ⊆ t i) (htn : ∀ (i : ℕ), (t i).Nonempty) (ht0 : IsCompact (t 0)) (htcl : ∀ (i : ℕ), IsClosed (t i)) : (⋂ i, t i).Nonempty
• IsCompact.compl_mem_sets 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {f : Filter X} (hf : ∀ x ∈ s, sᶜ ∈ nhds x ⊓ f) : sᶜ ∈ f
• IsCompact.tendsto_nhds_of_unique_mapClusterPt 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} {Y : Type u_2} {l : Filter Y} {y : X} {f : Y → X} (hs : IsCompact s) (hmem : ∀ᶠ (x : Y) in l, f x ∈ s) (h : ∀ x ∈ s, MapClusterPt x l f → x = y) : Filter.Tendsto f l (nhds y)
• IsCompact.mem_inf_nhdsSet_of_forall 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {K : Set X} {l : Filter X} {s : Set X} (hK : IsCompact K) (hs : ∀ y ∈ K, s ∈ l ⊓ nhds y) : s ∈ l ⊓ nhdsSet K
• IsCompact.mem_nhdsSet_inf_of_forall 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {K : Set X} {l : Filter X} {s : Set X} (hK : IsCompact K) (hs : ∀ x ∈ K, s ∈ nhds x ⊓ l) : s ∈ nhdsSet K ⊓ l
• IsCompact.ultrafilter_le_nhds 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsCompact s → ∀ (f : Ultrafilter X), ↑f ≤ Filter.principal s → ∃ x ∈ s, ↑f ≤ nhds x
• isCompact_iff_ultrafilter_le_nhds 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsCompact s ↔ ∀ (f : Ultrafilter X), ↑f ≤ Filter.principal s → ∃ x ∈ s, ↑f ≤ nhds x
• IsCompact.elim_directed_cover 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} {ι : Type v} [hι : Nonempty ι] (hs : IsCompact s) (U : ι → Set X) (hUo : ∀ (i : ι), IsOpen (U i)) (hsU : s ⊆ ⋃ i, U i) (hdU : Directed (fun x1 x2 => x1 ⊆ x2) U) : ∃ i, s ⊆ U i
• IsCompact.le_nhdsSet_of_clusterPt 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {l : Filter X} {s' : Set X} (hmem : s ∈ l) (h : ∀ x ∈ s, ClusterPt x l → x ∈ s') : l ≤ nhdsSet s'
• Finset.isCompact_biUnion 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {ι : Type u_1} [TopologicalSpace X] (s : Finset ι) {f : ι → Set X} (hf : ∀ i ∈ s, IsCompact (f i)) : IsCompact (⋃ i ∈ s, f i)
• IsCompact.inf_nhdsSet_eq_biSup 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) (l : Filter X) : l ⊓ nhdsSet K = ⨆ x ∈ K, l ⊓ nhds x
• IsCompact.nhdsSet_inf_eq_biSup 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) (l : Filter X) : nhdsSet K ⊓ l = ⨆ x ∈ K, nhds x ⊓ l
• IsCompact.tendsto_nhdsSet_of_mapClusterPt 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} {Y : Type u_2} {l : Filter Y} {s' : Set X} {f : Y → X} (hs : IsCompact s) (hmem : ∀ᶠ (x : Y) in l, f x ∈ s) (h : ∀ x ∈ s, MapClusterPt x l f → x ∈ s') : Filter.Tendsto f l (nhdsSet s')
• IsCompact.adherence_nhdset 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s t : Set X} {f : Filter X} (hs : IsCompact s) (hf₂ : f ≤ Filter.principal s) (ht₁ : IsOpen t) (ht₂ : ∀ x ∈ s, ClusterPt x f → x ∈ t) : t ∈ f
• IsCompact.nhdsSet_prod_eq 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} (hs : IsCompact s) (ht : IsCompact t) : nhdsSet (s ×ˢ t) = nhdsSet s ×ˢ nhdsSet t
• IsCompact.sigma_exists_finite_sigma_eq 📋 Mathlib.Topology.Compactness.Compact
  {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] (u : Set ((i : ι) × X i)) (hu : IsCompact u) : ∃ s t, s.Finite ∧ (∀ (i : ι), IsCompact (t i)) ∧ s.sigma t = u
• exists_subset_nhds_of_isCompact' 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {ι : Type u_1} [TopologicalSpace X] [Nonempty ι] {V : ι → Set X} (hV : Directed (fun x1 x2 => x1 ⊇ x2) V) (hV_cpct : ∀ (i : ι), IsCompact (V i)) (hV_closed : ∀ (i : ι), IsClosed (V i)) {U : Set X} (hU : U ∈ nhdsSet (⋂ i, V i)) : ∃ i, V i ⊆ U
• IsCompact.compl_mem_sets_of_nhdsWithin 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {f : Filter X} (hf : ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, tᶜ ∈ f) : sᶜ ∈ f
• IsCompact.nonempty_inter_sInter 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {t : Set (Set X)} (ht : ∀ a ∈ t, IsClosed a) (h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty) : (s ∩ ⋂₀ t).Nonempty
• isCompact_generateFrom 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [T : TopologicalSpace X] {S : Set (Set X)} (hTS : T = TopologicalSpace.generateFrom S) {s : Set X} (h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q) : IsCompact s
• IsCompact.disjoint_nhdsSet_left 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} {l : Filter X} (hs : IsCompact s) : Disjoint (nhdsSet s) l ↔ ∀ x ∈ s, Disjoint (nhds x) l
• IsCompact.disjoint_nhdsSet_right 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} {l : Filter X} (hs : IsCompact s) : Disjoint l (nhdsSet s) ↔ ∀ x ∈ s, Disjoint l (nhds x)
• isCompact_of_finite_subcover 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (h : ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i) : IsCompact s
• IsCompact.elim_finite_subcover 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} {ι : Type v} (hs : IsCompact s) (U : ι → Set X) (hUo : ∀ (i : ι), IsOpen (U i)) (hsU : s ⊆ ⋃ i, U i) : ∃ t, s ⊆ ⋃ i ∈ t, U i
• IsCompact.eventually_forall_of_forall_eventually 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x₀ : X} {K : Set Y} (hK : IsCompact K) {P : X → Y → Prop} (hP : ∀ y ∈ K, ∀ᶠ (z : X × Y) in nhds (x₀, y), P z.1 z.2) : ∀ᶠ (x : X) in nhds x₀, ∀ y ∈ K, P x y
• isCompact_iff_finite_subcover 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsCompact s ↔ ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i
• IsCompact.inter_iInter_nonempty 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} {ι : Type v} (hs : IsCompact s) (t : ι → Set X) (htc : ∀ (i : ι), IsClosed (t i)) (hst : ∀ (u : Finset ι), (s ∩ ⋂ i ∈ u, t i).Nonempty) : (s ∩ ⋂ i, t i).Nonempty
• Pi.exists_compact_superset_iff 📋 Mathlib.Topology.Compactness.Compact
  {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {s : Set ((i : ι) → X i)} : (∃ K, IsCompact K ∧ s ⊆ K) ↔ ∀ (i : ι), ∃ Ki, IsCompact Ki ∧ s ⊆ Function.eval i ⁻¹' Ki
• IsCompact.elim_directedOn_cover 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (U : Set (Set X)) (hUo : ∀ u ∈ U, IsOpen u) (hsU : s ⊆ ⋃₀ U) (hdU : DirectedOn (fun x1 x2 => x1 ⊆ x2) U) (hU : U.Nonempty) : ∃ u ∈ U, s ⊆ u
• IsCompact.induction_on 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {p : Set X → Prop} (he : p ∅) (hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s) (hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)) (hnhds : ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, p t) : p s
• IsCompact.nonempty_sInter_of_directed_nonempty_isCompact_isClosed 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {S : Set (Set X)} [hS : Nonempty ↑S] (hSd : DirectedOn (fun x1 x2 => x1 ⊇ x2) S) (hSn : ∀ U ∈ S, U.Nonempty) (hSc : ∀ U ∈ S, IsCompact U) (hScl : ∀ U ∈ S, IsClosed U) : (⋂₀ S).Nonempty
• IsCompact.nhdsSetWithin_prod_eq 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s s' : Set X} {t t' : Set Y} (hs : IsCompact s) (ht : IsCompact t) : nhdsSetWithin (s ×ˢ t) (s' ×ˢ t') = nhdsSetWithin s s' ×ˢ nhdsSetWithin t t'
• IsCompact.mem_nhdsSet_prod_of_forall 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {K : Set X} {Y : Type u_2} {l : Filter Y} {s : Set (X × Y)} (hK : IsCompact K) (hs : ∀ x ∈ K, s ∈ nhds x ×ˢ l) : s ∈ nhdsSet K ×ˢ l
• IsCompact.mem_prod_nhdsSet_of_forall 📋 Mathlib.Topology.Compactness.Compact
  {Y : Type v} [TopologicalSpace Y] {K : Set Y} {X : Type u_2} {l : Filter X} {s : Set (X × Y)} (hK : IsCompact K) (hs : ∀ y ∈ K, s ∈ l ×ˢ nhds y) : s ∈ l ×ˢ nhdsSet K
• IsCompact.nhdsSet_prod_eq_biSup 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) {Y : Type u_2} (l : Filter Y) : nhdsSet K ×ˢ l = ⨆ x ∈ K, nhds x ×ˢ l
• IsCompact.prod_nhdsSet_eq_biSup 📋 Mathlib.Topology.Compactness.Compact
  {Y : Type v} [TopologicalSpace Y] {K : Set Y} (hK : IsCompact K) {X : Type u_2} (l : Filter X) : l ×ˢ nhdsSet K = ⨆ y ∈ K, l ×ˢ nhds y
• nhdsSet_prod_le_of_disjoint_cocompact 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : Filter Y} (hs : IsCompact s) (hf : Disjoint f (Filter.cocompact Y)) : nhdsSet s ×ˢ f ≤ nhdsSet (s ×ˢ Set.univ)
• prod_nhdsSet_le_of_disjoint_cocompact 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {t : Set Y} {f : Filter X} (ht : IsCompact t) (hf : Disjoint f (Filter.cocompact X)) : f ×ˢ nhdsSet t ≤ nhdsSet (Set.univ ×ˢ t)
• IsCompact.elim_nhds_subcover 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (U : X → Set X) (hU : ∀ x ∈ s, U x ∈ nhds x) : ∃ t, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
• IsCompact.elim_nhdsWithin_subcover 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (U : X → Set X) (hU : ∀ x ∈ s, U x ∈ nhdsWithin x s) : ∃ t, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
• IsCompact.elim_nhds_subcover_nhdsSet 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {U : X → Set X} (hU : ∀ x ∈ s, U x ∈ nhds x) : ∃ t, (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ nhdsSet s
• IsCompact.elim_finite_subcover_image 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {ι : Type u_1} [TopologicalSpace X] {s : Set X} {b : Set ι} {c : ι → Set X} (hs : IsCompact s) (hc₁ : ∀ i ∈ b, IsOpen (c i)) (hc₂ : s ⊆ ⋃ i ∈ b, c i) : ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i
• isCompact_generateFrom' 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [T : TopologicalSpace X] {S : Set (Set X)} (hTS : T = TopologicalSpace.generateFrom S) {s : Set X} (h : ∀ (ι : Type u) (U : ι → ↑S), s ⊆ ⋃ i, ↑(U i) → ∃ J, J.Finite ∧ s ⊆ ⋃ i ∈ J, ↑(U i)) : IsCompact s
• generalized_tube_lemma 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (hs : IsCompact s) {t : Set Y} (ht : IsCompact t) {n : Set (X × Y)} (hn : IsOpen n) (hp : s ×ˢ t ⊆ n) : ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n
• generalized_tube_lemma_left 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s s' : Set X} (hs : IsCompact s) {t : Set Y} (ht : IsCompact t) {n : Set (X × Y)} (hn : n ∈ nhdsSetWithin (s ×ˢ t) (s' ×ˢ t)) : ∃ u ∈ nhdsSetWithin s s', u ×ˢ t ⊆ n
• generalized_tube_lemma_right 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (hs : IsCompact s) {t t' : Set Y} (ht : IsCompact t) {n : Set (X × Y)} (hn : n ∈ nhdsSetWithin (s ×ˢ t) (s ×ˢ t')) : ∃ u ∈ nhdsSetWithin t t', s ×ˢ u ⊆ n
• IsCompact.elim_directed_family_closed 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} {ι : Type v} [Nonempty ι] (hs : IsCompact s) (t : ι → Set X) (htc : ∀ (i : ι), IsClosed (t i)) (hst : Disjoint s (⋂ i, t i)) (hdt : Directed (fun x1 x2 => x1 ⊇ x2) t) : ∃ i, Disjoint s (t i)
• IsCompact.elim_nhds_subcover' 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (U : (x : X) → x ∈ s → Set X) (hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ nhds x) : ∃ t, s ⊆ ⋃ x ∈ t, U ↑x ⋯
• IsCompact.elim_nhdsWithin_subcover' 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (U : (x : X) → x ∈ s → Set X) (hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ nhdsWithin x s) : ∃ t, s ⊆ ⋃ x ∈ t, U ↑x ⋯
• generalized_tube_lemma' 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s s' : Set X} (hs : IsCompact s) {t t' : Set Y} (ht : IsCompact t) {n : Set (X × Y)} (hn : n ∈ nhdsSetWithin (s ×ˢ t) (s' ×ˢ t')) : ∃ u ∈ nhdsSetWithin s s', ∃ v ∈ nhdsSetWithin t t', u ×ˢ v ⊆ n
• IsCompact.elim_nhds_subcover_nhdsSet' 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (U : (x : X) → x ∈ s → Set X) (hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ nhds x) : ∃ t, ⋃ x ∈ t, U ↑x ⋯ ∈ nhdsSet s
• isCompact_of_finite_subfamily_closed 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → Disjoint s (⋂ i, t i) → ∃ u, Disjoint s (⋂ i ∈ u, t i)) : IsCompact s
• IsCompact.elim_finite_subfamily_closed 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} {ι : Type v} (hs : IsCompact s) (t : ι → Set X) (htc : ∀ (i : ι), IsClosed (t i)) (hst : Disjoint s (⋂ i, t i)) : ∃ u, Disjoint s (⋂ i ∈ u, t i)
• isCompact_iff_finite_subfamily_closed 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsCompact s ↔ ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → Disjoint s (⋂ i, t i) → ∃ u, Disjoint s (⋂ i ∈ u, t i)
• IsCompact.elim_finite_subfamily_isClosed_subtype 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u_2} [TopologicalSpace X] {s : Set X} (ks : IsCompact s) {ι : Type u_3} (t : ι → Set X) {I : Set ι} (htc : ∀ i ∈ I, IsClosed (Subtype.val ⁻¹' t i)) (hst : Disjoint s (⋂ i ∈ I, t i)) : ∃ u, Disjoint s (⋂ i ∈ u, t ↑i)
• exists_compact_superset 📋 Mathlib.Topology.Compactness.LocallyCompact
  {X : Type u_1} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] {K : Set X} (hK : IsCompact K) : ∃ K', IsCompact K' ∧ K ⊆ interior K'
• compact_basis_nhds 📋 Mathlib.Topology.Compactness.LocallyCompact
  {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] (x : X) : (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsCompact s) fun s => s
• IsCompact.nhdsSet_basis_isCompact 📋 Mathlib.Topology.Compactness.LocallyCompact
  {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] {K : Set X} (hK : IsCompact K) : (nhdsSet K).HasBasis (fun L => L ∈ nhdsSet K ∧ IsCompact L) id
• LocallyCompactSpace.of_hasBasis 📋 Mathlib.Topology.Compactness.LocallyCompact
  {X : Type u_1} [TopologicalSpace X] {ι : X → Type u_4} {p : (x : X) → ι x → Prop} {s : (x : X) → ι x → Set X} (h : ∀ (x : X), (nhds x).HasBasis (p x) (s x)) (hc : ∀ (x : X) (i : ι x), p x i → IsCompact (s x i)) : LocallyCompactSpace X
• exists_compact_subset 📋 Mathlib.Topology.Compactness.LocallyCompact
  {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] {x : X} {U : Set X} (hU : IsOpen U) (hx : x ∈ U) : ∃ K, IsCompact K ∧ x ∈ interior K ∧ K ⊆ U
• local_compact_nhds 📋 Mathlib.Topology.Compactness.LocallyCompact
  {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] {x : X} {n : Set X} (h : n ∈ nhds x) : ∃ s ∈ nhds x, s ⊆ n ∧ IsCompact s
• exists_compact_between 📋 Mathlib.Topology.Compactness.LocallyCompact
  {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] {K U : Set X} (hK : IsCompact K) (hU : IsOpen U) (h_KU : K ⊆ U) : ∃ L, IsCompact L ∧ K ⊆ interior L ∧ L ⊆ U
• exists_mem_nhdsSet_isCompact_mapsTo 📋 Mathlib.Topology.Compactness.LocallyCompact
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactPair X Y] {f : X → Y} {K : Set X} {U : Set Y} (hf : Continuous f) (hK : IsCompact K) (hU : IsOpen U) (hKU : Set.MapsTo f K U) : ∃ L ∈ nhdsSet K, IsCompact L ∧ Set.MapsTo f L U
• LocallyFinite.finite_nonempty_inter_compact 📋 Mathlib.Topology.Compactness.LocallyFinite
  {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] {s : Set X} {f : ι → Set X} (hf : LocallyFinite f) (hs : IsCompact s) : {i | (f i ∩ s).Nonempty}.Finite
• IsCompact.isSigmaCompact 📋 Mathlib.Topology.Compactness.SigmaCompact
  {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) : IsSigmaCompact s
• isCompact_compactCovering 📋 Mathlib.Topology.Compactness.SigmaCompact
  (X : Type u_1) [TopologicalSpace X] [SigmaCompactSpace X] (n : ℕ) : IsCompact (compactCovering X n)
• CompactExhaustion.isCompact' 📋 Mathlib.Topology.Compactness.SigmaCompact
  {X : Type u_4} [TopologicalSpace X] (self : CompactExhaustion X) (n : ℕ) : IsCompact (self.toFun n)
• CompactExhaustion.isCompact 📋 Mathlib.Topology.Compactness.SigmaCompact
  {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) (n : ℕ) : IsCompact (K n)
• isSigmaCompact_iUnion_of_isCompact 📋 Mathlib.Topology.Compactness.SigmaCompact
  {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] [hι : Countable ι] (s : ι → Set X) (hcomp : ∀ (i : ι), IsCompact (s i)) : IsSigmaCompact (⋃ i, s i)
• SigmaCompactSpace.exists_compact_covering 📋 Mathlib.Topology.Compactness.SigmaCompact
  {X : Type u_1} [TopologicalSpace X] [h : SigmaCompactSpace X] : ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = Set.univ
• SigmaCompactSpace_iff_exists_compact_covering 📋 Mathlib.Topology.Compactness.SigmaCompact
  {X : Type u_1} [TopologicalSpace X] : SigmaCompactSpace X ↔ ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = Set.univ
• isSigmaCompact_sUnion_of_isCompact 📋 Mathlib.Topology.Compactness.SigmaCompact
  {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} (hc : S.Countable) (hcomp : ∀ s ∈ S, IsCompact s) : IsSigmaCompact (⋃₀ S)
• CompactExhaustion.exists_superset_of_isCompact 📋 Mathlib.Topology.Compactness.SigmaCompact
  {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) {s : Set X} (hs : IsCompact s) : ∃ n, s ⊆ K n
• SigmaCompactSpace.of_countable 📋 Mathlib.Topology.Compactness.SigmaCompact
  {X : Type u_1} [TopologicalSpace X] (S : Set (Set X)) (Hc : S.Countable) (Hcomp : ∀ s ∈ S, IsCompact s) (HU : ⋃₀ S = Set.univ) : SigmaCompactSpace X
• CompactExhaustion.mk 📋 Mathlib.Topology.Compactness.SigmaCompact
  {X : Type u_4} [TopologicalSpace X] (toFun : ℕ → Set X) (isCompact' : ∀ (n : ℕ), IsCompact (toFun n)) (subset_interior_succ' : ∀ (n : ℕ), toFun n ⊆ interior (toFun (n + 1))) (iUnion_eq' : ⋃ n, toFun n = Set.univ) : CompactExhaustion X
• IsCompact.of_subset_of_specializes 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {s t : Set X} (hs : IsCompact s) (hts : t ⊆ s) (h : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y) : IsCompact t
• Set.Finite.isCompact_closure 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R0Space X] {s : Set X} (hs : s.Finite) : IsCompact (closure s)
• IsCompact.closure 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} (hK : IsCompact K) : IsCompact (closure K)
• isCompact_closure_singleton 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R0Space X] {x : X} : IsCompact (closure {x})
• Bornology.relativelyCompact.isBounded_iff 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R0Space X] {s : Set X} : Bornology.IsBounded s ↔ IsCompact (closure s)
• IsCompact.closure_of_subset 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {s K : Set X} (hK : IsCompact K) (h : s ⊆ K) : IsCompact (closure s)
• exists_isCompact_superset_iff 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {s : Set X} : (∃ K, IsCompact K ∧ s ⊆ K) ↔ IsCompact (closure s)
• IsCompact.closure_subset_of_isOpen 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} (hK : IsCompact K) {U : Set X} (hU : IsOpen U) (hKU : K ⊆ U) : closure K ⊆ U
• exists_isOpen_mem_isCompact_closure 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] (x : X) : ∃ U, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U)
• exists_mem_nhds_isCompact_isClosed 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] (x : X) : ∃ K ∈ nhds x, IsCompact K ∧ IsClosed K
• exists_isOpen_superset_and_isCompact_closure 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] {K : Set X} (hK : IsCompact K) : ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V)
• IsCompact.mem_closure_iff_exists_inseparable 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {y : X} {K : Set X} (hK : IsCompact K) : y ∈ closure K ↔ ∃ x ∈ K, Inseparable x y
• isCompact_isClosed_basis_nhds 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] (x : X) : (nhds x).HasBasis (fun K => K ∈ nhds x ∧ IsCompact K ∧ IsClosed K) fun x => x
• IsCompact.closure_eq_biUnion_inseparable 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} (hK : IsCompact K) : closure K = ⋃ x ∈ K, {y | Inseparable x y}
• IsCompact.closure_eq_biUnion_closure_singleton 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} (hK : IsCompact K) : closure K = ⋃ x ∈ K, closure {x}
• IsCompact.isCompact_isClosed_basis_nhds 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {x : X} {L : Set X} (hLc : IsCompact L) (hxL : L ∈ nhds x) : (nhds x).HasBasis (fun K => K ∈ nhds x ∧ IsCompact K ∧ IsClosed K) fun x => x
• SeparatedNhds.of_isCompact_isCompact_isClosed 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {K L : Set X} (hK : IsCompact K) (hL : IsCompact L) (h'L : IsClosed L) (hd : Disjoint K L) : SeparatedNhds K L
• exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [R1Space Y] {f : X → Y} {x : X} {K : Set X} {s : Set Y} (hf : Continuous f) (hs : s ∈ nhds (f x)) (hKc : IsCompact K) (hKx : K ∈ nhds x) : ∃ L ∈ nhds x, IsCompact L ∧ Set.MapsTo f L s
• IsCompact.binary_compact_cover 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {K U V : Set X} (hK : IsCompact K) (hU : IsOpen U) (hV : IsOpen V) (h2K : K ⊆ U ∪ V) : ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂
• IsCompact.finite_compact_cover 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {s : Set X} (hs : IsCompact s) {ι : Type u_3} (t : Finset ι) (U : ι → Set X) (hU : ∀ i ∈ t, IsOpen (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i) : ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
• tendsto_cofinite_cocompact_iff 📋 Mathlib.Topology.DiscreteSubset
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace Y] {f : X → Y} : Filter.Tendsto f Filter.cofinite (Filter.cocompact Y) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite
• IsCompact.codiscreteWithin_eq 📋 Mathlib.Topology.DiscreteSubset
  {X : Type u_1} [TopologicalSpace X] {K : Set X} [T1Space X] (hK : IsCompact K) : Filter.codiscreteWithin K = Filter.cofinite ⊓ Filter.principal K
• IsCompact.finite_diff_of_mem_codiscreteWithin 📋 Mathlib.Topology.DiscreteSubset
  {X : Type u_1} [TopologicalSpace X] {s K : Set X} (hK : IsCompact K) (hs : s ∈ Filter.codiscreteWithin K) : (K \ s).Finite
• IsCompact.finite_sdiff_of_mem_codiscreteWithin 📋 Mathlib.Topology.DiscreteSubset
  {X : Type u_1} [TopologicalSpace X] {s K : Set X} (hK : IsCompact K) (hs : s ∈ Filter.codiscreteWithin K) : (K \ s).Finite
• IsCompact.cofinite_inf_le_codiscreteWithin 📋 Mathlib.Topology.DiscreteSubset
  {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) : Filter.cofinite ⊓ Filter.principal K ≤ Filter.codiscreteWithin K
• IsCompact.isClosed 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} (hs : IsCompact s) : IsClosed s
• IsCompact.inter 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ∩ t)
• 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)
• IsCompact.nhdsSet_inter_eq 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) : nhdsSet (s ∩ t) = nhdsSet s ⊓ nhdsSet t
• image_closure_of_isCompact 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {s : Set X} (hs : IsCompact (closure s)) {f : X → Y} (hf : ContinuousOn f (closure s)) : f '' closure s = closure (f '' s)
• IsCompact.disjoint_nhdsSet_nhds 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {t : Set X} (H1 : IsCompact t) (H2 : x ∉ t) : Disjoint (nhdsSet t) (nhds x)
• Pi.isCompact_iff 📋 Mathlib.Topology.Separation.Hausdorff
  {ι : Type u_4} {X : ι → Type u_5} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T2Space (X i)] {s : Set ((i : ι) → X i)} : IsCompact s ↔ IsClosed s ∧ ∀ (i : ι), IsCompact (Function.eval i '' s)
• Pi.isCompact_closure_iff 📋 Mathlib.Topology.Separation.Hausdorff
  {ι : Type u_4} {X : ι → Type u_5} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), R1Space (X i)] {s : Set ((i : ι) → X i)} : IsCompact (closure s) ↔ ∀ (i : ι), IsCompact (closure (Function.eval i '' s))
• exists_subset_nhds_of_isCompact 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [T2Space X] {ι : Type u_4} [Nonempty ι] {V : ι → Set X} (hV : Directed (fun x1 x2 => x1 ⊇ x2) V) (hV_cpct : ∀ (i : ι), IsCompact (V i)) {U : Set X} (hU : U ∈ nhdsSet (⋂ i, V i)) : ∃ i, V i ⊆ U
• SeparatedNhds.of_isCompact_isCompact 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) (hst : Disjoint s t) : SeparatedNhds s t
• SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {s t : Set X} (H1 : IsClosed s) (H2 : IsCompact (closure sᶜ)) (H3 : IsClosed t) (H4 : Disjoint s t) : SeparatedNhds s t
• Set.InjOn.exists_isOpen_superset 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} {s : Set X} (inj : Set.InjOn f s) (sc : IsCompact s) (fc : ∀ x ∈ s, ContinuousAt f x) (loc : ∀ x ∈ s, ∃ u ∈ nhds x, Set.InjOn f u) : ∃ t, IsOpen t ∧ s ⊆ t ∧ Set.InjOn f t
• Set.InjOn.exists_mem_nhdsSet 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} {s : Set X} (inj : Set.InjOn f s) (sc : IsCompact s) (fc : ∀ x ∈ s, ContinuousAt f x) (loc : ∀ x ∈ s, ∃ u ∈ nhds x, Set.InjOn f u) : ∃ t ∈ nhdsSet s, Set.InjOn f t
• IsCompact.separation_of_notMem 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {t : Set X} (H1 : IsCompact t) (H2 : x ∉ t) : ∃ U V, IsOpen U ∧ IsOpen V ∧ t ⊆ U ∧ x ∈ V ∧ Disjoint U V
• t2_separation_compact_nhds 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [T2Space X] {x y : X} (h : x ≠ y) : ∃ u v, u ∈ nhds x ∧ v ∈ nhds y ∧ IsCompact u ∧ IsCompact v ∧ Disjoint u v
• IsCompact.isLindelof 📋 Mathlib.Topology.Compactness.Lindelof
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) : IsLindelof s
• IsCompact.closure_eq_nhdsKer 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {s : Set X} (hs : IsCompact s) : closure s = nhdsKer s
• IsCompact.lift'_closure_nhdsSet 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {K : Set X} (hK : IsCompact K) : (nhdsSet K).lift' closure = nhdsSet K
• IsCompact.nhdsSet_basis_isCompact_isClosed 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [RegularSpace X] {K : Set X} (hK : IsCompact K) : (nhdsSet K).HasBasis (fun L => L ∈ nhdsSet K ∧ IsCompact L ∧ IsClosed L) id
• IsCompact.exists_isOpen_closure_subset 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {K U : Set X} (hK : IsCompact K) (hU : U ∈ nhdsSet K) : ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U
• exists_compact_closed_between 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [RegularSpace X] {K U : Set X} (hK : IsCompact K) (hU : IsOpen U) (h_KU : K ⊆ U) : ∃ L, IsCompact L ∧ IsClosed L ∧ K ⊆ interior L ∧ L ⊆ U
• exists_open_between_and_isCompact_closure 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [RegularSpace X] {K U : Set X} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. 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 9f11169 serving mathlib revision ce5dd8c