Compact

📁 Source: Mathlib/Topology/Compactness/Compact.lean

Statistics

Metric	Count
Definitions inCompact	1
Theorems isBounded_iff, elim_nhds_subcover, iInter_nonempty, isCompact_insert_range, isCompact_insert_range_of_cocompact, isCompact_insert_range_of_cofinite, cocompact_eq_bot, cocompact_eq_cofinite, cocompact_le_coclosedCompact, cocompact_le_cofinite, cocompact_neBot_iff, comap_cocompact_le, compl_mem_coclosedCompact, coprod_cocompact, coprodᵢ_cocompact, disjoint_cocompact_left, disjoint_cocompact_right, hasBasis_coclosedCompact, hasBasis_cocompact, mem_coclosedCompact_iff, mem_cocompact, mem_cocompact', compactSpace, isCompact_biUnion, compactSpace, exists_minimal_nonempty_closed_subset, isCompact, adherence_nhdset, compl_mem_coclosedCompact_of_isClosed, compl_mem_cocompact, compl_mem_sets, compl_mem_sets_of_nhdsWithin, diff, disjoint_nhdsSet_left, disjoint_nhdsSet_right, elim_directed_cover, elim_directed_family_closed, elim_finite_subcover, elim_finite_subcover_image, elim_finite_subfamily_closed, elim_finite_subfamily_isClosed_subtype, elim_nhdsWithin_subcover, elim_nhdsWithin_subcover', elim_nhds_subcover, elim_nhds_subcover', elim_nhds_subcover_nhdsSet, elim_nhds_subcover_nhdsSet', eventually_forall_of_forall_eventually, exists_clusterPt, exists_clusterPt_of_frequently, exists_mapClusterPt, exists_mapClusterPt_of_frequently, finite, finite_of_discrete, image, image_of_continuousOn, induction_on, inf_nhdsSet_eq_biSup, insert, inter_iInter_nonempty, inter_left, inter_right, le_nhds_of_unique_clusterPt, mem_inf_nhdsSet_of_forall, mem_nhdsSet_inf_of_forall, mem_nhdsSet_prod_of_forall, mem_prod_nhdsSet_of_forall, ne_univ, nhdsSetWithin_prod_eq, nhdsSet_inf_eq_biSup, nhdsSet_prod_eq, nhdsSet_prod_eq_biSup, nonempty_iInter_of_directed_nonempty_isCompact_isClosed, nonempty_iInter_of_sequence_nonempty_isCompact_isClosed, nonempty_sInter_of_directed_nonempty_isCompact_isClosed, of_isClosed_subset, prod, prod_nhdsSet_eq_biSup, sigma_exists_finite_sigma_eq, tendsto_nhds_of_unique_mapClusterPt, ultrafilter_le_nhds, ultrafilter_le_nhds', union, compactSpace, exists_compact_superset_iff, isCompact_iff_of_isClosed, noncompactSpace_iff, noncompactSpace_left, noncompactSpace_right, compactSpace, compactSpace, isCompact, isCompact_biUnion, isCompact_sUnion, exists_accPt_cofinite_inf_principal, exists_accPt_cofinite_inf_principal_of_subset_isCompact, exists_accPt_of_subset_isCompact, exists_accPt_principal, isCompact, isCompact_sigma, sUnion_isCompact_eq_univ, compactSpace, isCompact_iff, compactSpace, isCompact_preimage, noncompactSpace, tendsto_cocompact, isCompact_iff, isCompact_iff, isCompact_preimage, isCompact_preimage', isCompact_preimage_iff, compactSpace, le_nhds_lim, compactSpace_generateFrom, compactSpace_generateFrom', compactSpace_of_finite_subfamily_closed, disjoint_map_cocompact, exists_clusterPt_of_compactSpace, exists_nhds_ne_inf_principal_neBot, exists_nhds_ne_neBot, exists_subset_nhds_of_compactSpace, exists_subset_nhds_of_isCompact', finite_cover_nhds, finite_cover_nhds_interior, finite_of_compact_of_discrete, generalized_tube_lemma, generalized_tube_lemma', generalized_tube_lemma_left, generalized_tube_lemma_right, instCompactSpaceProd, instCompactSpaceSigmaOfFinite, instCompactSpaceSum, instNeBotCoclosedCompactOfNoncompactSpace, instNeBotCocompactOfNoncompactSpace, instNoncompactSpaceInt, isCompact_accumulate, isCompact_diagonal, isCompact_empty, isCompact_generateFrom, isCompact_generateFrom', isCompact_iUnion, isCompact_iff_compactSpace, isCompact_iff_finite, isCompact_iff_finite_subcover, isCompact_iff_finite_subfamily_closed, isCompact_iff_isCompact_univ, isCompact_iff_ultrafilter_le_nhds, isCompact_iff_ultrafilter_le_nhds', isCompact_of_finite_subcover, isCompact_of_finite_subfamily_closed, isCompact_pi_infinite, isCompact_range, isCompact_singleton, isCompact_univ, isCompact_univ_iff, isCompact_univ_pi, le_nhds_of_unique_clusterPt, nhdsSet_prod_le_of_disjoint_cocompact, nhds_prod_le_of_disjoint_cocompact, noncompactSpace_of_neBot, noncompact_univ, not_compactSpace_iff, prod_nhdsSet_le_of_disjoint_cocompact, prod_nhds_le_of_disjoint_cocompact, tendsto_nhds_of_unique_mapClusterPt	166
Total	167

Bornology

Definitions

Name	Category	Theorems
inCompact 📖	CompOp	2 math math: relativelyCompact_eq_inCompact, inCompact.isBounded_iff

Bornology.inCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBounded_iff 📖	mathematical	—	Bornology.IsBounded Bornology.inCompact IsCompact Set Set.instHasSubset	—	Filter.mem_cocompact

CompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
elim_nhds_subcover 📖	mathematical	Set Filter Filter.instMembership nhds	Set.iUnion Finset Finset.instMembership Top.top BooleanAlgebra.toTop Set.instBooleanAlgebra	—	IsCompact.elim_nhds_subcover isCompact_univ top_unique
iInter_nonempty 📖	—	IsClosed Set.Nonempty Set.iInter Finset Finset.instMembership	—	—	Set.univ_inter IsCompact.inter_iInter_nonempty isCompact_univ

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cocompact_eq_bot 📖	mathematical	—	cocompact Bot.bot Filter instBot	—	HasBasis.eq_bot_iff hasBasis_cocompact isCompact_univ Set.compl_univ
cocompact_eq_cofinite 📖	mathematical	—	cocompact cofinite	—	iInf_congr_Prop HasBasis.eq_biInf hasBasis_cofinite
cocompact_le_coclosedCompact 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder cocompact coclosedCompact	—	iInf_mono le_iInf le_rfl
cocompact_le_cofinite 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder cocompact cofinite	—	IsCompact.compl_mem_cocompact Set.Finite.isCompact compl_compl
cocompact_neBot_iff 📖	mathematical	—	NeBot cocompact NoncompactSpace	—	noncompactSpace_of_neBot instNeBotCocompactOfNoncompactSpace
comap_cocompact_le 📖	mathematical	Continuous	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder comap cocompact	—	HasBasis.le_basis_iff HasBasis.comap hasBasis_cocompact IsCompact.image Set.subset_preimage_image
compl_mem_coclosedCompact 📖	mathematical	—	Set Filter instMembership coclosedCompact Compl.compl Set.instCompl IsCompact closure	—	mem_coclosedCompact_iff compl_compl
coprod_cocompact 📖	mathematical	—	coprod cocompact instTopologicalSpaceProd	—	le_antisymm sup_le comap_cocompact_le continuous_fst continuous_snd HasBasis.ge_iff HasBasis.coprod hasBasis_cocompact Set.univ_prod Set.prod_univ Set.compl_prod_eq_union IsCompact.compl_mem_cocompact IsCompact.prod
coprodᵢ_cocompact 📖	mathematical	—	coprodᵢ cocompact Pi.topologicalSpace	—	le_antisymm iSup_le comap_cocompact_le continuous_apply Function.Surjective.forall compl_surjective isCompact_univ_pi
disjoint_cocompact_left 📖	mathematical	—	Disjoint Filter instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder instCompleteLatticeFilter cocompact Set instMembership IsCompact	—	HasBasis.disjoint_iff_left hasBasis_cocompact compl_compl
disjoint_cocompact_right 📖	mathematical	—	Disjoint Filter instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder instCompleteLatticeFilter cocompact Set instMembership IsCompact	—	HasBasis.disjoint_iff_right hasBasis_cocompact compl_compl
hasBasis_coclosedCompact 📖	mathematical	—	HasBasis Set coclosedCompact IsClosed IsCompact Compl.compl Set.instCompl	—	iInf_and' hasBasis_biInf_principal' IsClosed.union IsCompact.union Set.compl_subset_compl Set.subset_union_left Set.subset_union_right isClosed_empty isCompact_empty
hasBasis_cocompact 📖	mathematical	—	HasBasis Set cocompact IsCompact Compl.compl Set.instCompl	—	hasBasis_biInf_principal' IsCompact.union Set.compl_subset_compl Set.subset_union_left Set.subset_union_right isCompact_empty
mem_coclosedCompact_iff 📖	mathematical	—	Set Filter instMembership coclosedCompact IsCompact closure Compl.compl Set.instCompl	—	HasBasis.mem_iff hasBasis_coclosedCompact IsCompact.of_isClosed_subset isClosed_closure closure_minimal Set.compl_subset_comm subset_closure
mem_cocompact 📖	mathematical	—	Set Filter instMembership cocompact IsCompact Set.instHasSubset Compl.compl Set.instCompl	—	HasBasis.mem_iff hasBasis_cocompact
mem_cocompact' 📖	mathematical	—	Set Filter instMembership cocompact IsCompact Set.instHasSubset Compl.compl Set.instCompl	—	mem_cocompact Set.compl_subset_comm

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact_insert_range 📖	mathematical	Filter.Tendsto Filter.atTop Nat.instPreorder nhds	IsCompact Set Set.instInsert Set.range	—	isCompact_insert_range_of_cofinite Nat.cofinite_eq_atTop
isCompact_insert_range_of_cocompact 📖	mathematical	Filter.Tendsto Filter.cocompact nhds Continuous	IsCompact Set Set.instInsert Set.range	—	Filter.mem_cocompact Filter.mp_mem Filter.le_principal_iff Filter.univ_mem' Disjoint.le_bot mem_of_mem_nhds Set.mem_image_of_mem IsCompact.image Set.image_subset_range
isCompact_insert_range_of_cofinite 📖	mathematical	Filter.Tendsto Filter.cofinite nhds	IsCompact Set Set.instInsert Set.range	—	isCompact_insert_range_of_cocompact Filter.cocompact_eq_cofinite continuous_of_discreteTopology

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace 📖	mathematical	—	CompactSpace	—	Set.Finite.isCompact Set.finite_univ

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact_biUnion 📖	mathematical	IsCompact	Set.iUnion Finset instMembership	—	Set.Finite.isCompact_biUnion finite_toSet

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace 📖	mathematical	—	CompactSpace Pi.topologicalSpace	—	Pi.compactSpace

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_minimal_nonempty_closed_subset 📖	mathematical	Set.Nonempty	Set Set.instHasSubset IsClosed	—	zorn_subset isOpen_sUnion Set.ext IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed IsChain.directedOn Set.instReflSubset Set.compl_subset_compl isCompact IsOpen.isClosed_compl Set.Subset.refl isOpen_compl_iff compl_compl Maximal.prop Set.compl_subset_comm Maximal.eq_of_ge Set.Subset.trans Set.subset_compl_comm
isCompact 📖	mathematical	—	IsCompact	—	IsCompact.of_isClosed_subset isCompact_univ Set.subset_univ

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adherence_nhdset 📖	mathematical	IsCompact Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.principal IsOpen Set Set.instMembership	Filter.instMembership	—	Classical.by_cases Filter.mem_of_eq_bot inf_le_of_left_le ClusterPt.of_inf_left inter_mem_nhdsWithin IsOpen.mem_nhds Filter.empty_mem_iff_bot Set.compl_inter_self Filter.NeBot.ne ClusterPt.of_inf_right
compl_mem_coclosedCompact_of_isClosed 📖	mathematical	IsCompact	Set Filter Filter.instMembership Filter.coclosedCompact Compl.compl Set.instCompl	—	Filter.HasBasis.mem_of_mem Filter.hasBasis_coclosedCompact
compl_mem_cocompact 📖	mathematical	IsCompact	Set Filter Filter.instMembership Filter.cocompact Compl.compl Set.instCompl	—	Filter.HasBasis.mem_of_mem Filter.hasBasis_cocompact
compl_mem_sets 📖	—	IsCompact Set Filter Filter.instMembership Filter.instInf nhds Compl.compl Set.instCompl	—	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq compl_compl inf_assoc inf_le_right
compl_mem_sets_of_nhdsWithin 📖	—	IsCompact Set Filter Filter.instMembership nhdsWithin Compl.compl Set.instCompl	—	—	compl_mem_sets Filter.mem_inf_principal Filter.mem_inf_of_inter
diff 📖	mathematical	IsCompact IsOpen	Set Set.instSDiff	—	inter_right isClosed_compl_iff
disjoint_nhdsSet_left 📖	mathematical	IsCompact	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhdsSet nhds	—	Disjoint.mono_left nhds_le_nhdsSet elim_nhds_subcover IsOpen.mem_nhds Filter.HasBasis.disjoint_iff_left hasBasis_nhdsSet isOpen_biUnion Set.compl_iUnion₂ Filter.biInter_finset_mem nhds_basis_opens Function.sometimes_spec
disjoint_nhdsSet_right 📖	mathematical	IsCompact	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhdsSet nhds	—	disjoint_nhdsSet_left
elim_directed_cover 📖	—	IsCompact IsOpen Set Set.instHasSubset Set.iUnion Directed	—	—	induction_on Set.empty_subset HasSubset.Subset.trans Set.instIsTransSubset Set.union_subset Set.Subset.trans Set.mem_iUnion mem_nhdsWithin_of_mem_nhds IsOpen.mem_nhds Set.Subset.refl
elim_directed_family_closed 📖	—	IsCompact IsClosed Set Set.instInter Set.iInter Set.instEmptyCollection Directed Set.instHasSubset	—	—	elim_directed_cover IsClosed.isOpen_compl Directed.mono_comp Set.compl_subset_compl
elim_finite_subcover 📖	mathematical	IsCompact IsOpen Set Set.instHasSubset Set.iUnion	Finset Finset.instMembership	—	elim_directed_cover isOpen_biUnion Set.iUnion_eq_iUnion_finset directed_of_isDirected_le Finset.isDirected_le Set.biUnion_subset_biUnion_left
elim_finite_subcover_image 📖	mathematical	IsCompact IsOpen Set Set.instHasSubset Set.iUnion Set.instMembership	Set.Finite	—	elim_finite_subcover Set.biUnion_eq_iUnion Subtype.coe_preimage_self Set.Finite.image Finset.finite_toSet Set.biUnion_image
elim_finite_subfamily_closed 📖	mathematical	IsCompact IsClosed Set Set.instInter Set.iInter Set.instEmptyCollection	Finset Finset.instMembership	—	elim_directed_family_closed isClosed_biInter Set.iInter_eq_iInter_finset directed_of_isDirected_le Finset.isDirected_le Set.biInter_subset_biInter_left
elim_finite_subfamily_isClosed_subtype 📖	mathematical	IsCompact IsClosed Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.preimage Set.instInter Set.iInter Set.instEmptyCollection	Finset Finset.instMembership	—	Set.iInter_coe_set Set.iInter_congr_Prop Set.univ_inter elim_finite_subfamily_closed isCompact_iff_isCompact_univ Subtype.prop
elim_nhdsWithin_subcover 📖	mathematical	IsCompact Set Filter Filter.instMembership nhdsWithin	Set.instMembership Set.instHasSubset Set.iUnion Finset Finset.instMembership	—	subset_trans Set.instIsTransSubset Set.instReflSubset Set.iUnion₂_mono elim_nhds_subcover mem_nhdsWithin_iff_exists_mem_nhds_inter Function.sometimes_spec
elim_nhdsWithin_subcover' 📖	mathematical	IsCompact Set Filter Filter.instMembership nhdsWithin	Set.instHasSubset Set.iUnion Set.Elem Finset Finset.instMembership Set.instMembership	—	subset_trans Set.instIsTransSubset Set.instReflSubset Set.iUnion₂_mono elim_nhds_subcover' mem_nhdsWithin_iff_exists_mem_nhds_inter
elim_nhds_subcover 📖	mathematical	IsCompact Set Filter Filter.instMembership nhds	Set.instMembership Set.instHasSubset Set.iUnion Finset Finset.instMembership	—	subset_of_mem_nhdsSet elim_nhds_subcover_nhdsSet
elim_nhds_subcover' 📖	mathematical	IsCompact Set Filter Filter.instMembership nhds	Set.instHasSubset Set.iUnion Set.Elem Finset Finset.instMembership Set.instMembership	—	subset_of_mem_nhdsSet elim_nhds_subcover_nhdsSet'
elim_nhds_subcover_nhdsSet 📖	mathematical	IsCompact Set Filter Filter.instMembership nhds	Set.instMembership nhdsSet Set.iUnion Finset Finset.instMembership	—	elim_nhds_subcover_nhdsSet' Finset.mem_image Finset.set_biUnion_finset_image
elim_nhds_subcover_nhdsSet' 📖	mathematical	IsCompact Set Filter Filter.instMembership nhds	nhdsSet Set.iUnion Set.Elem Finset Finset.instMembership Set.instMembership	—	elim_finite_subcover isOpen_interior Set.mem_iUnion mem_interior_iff_mem_nhds mem_nhdsSet_iff_forall Set.mem_iUnion₂ Filter.mem_of_superset Set.subset_biUnion_of_mem
eventually_forall_of_forall_eventually 📖	—	IsCompact Filter.Eventually nhds instTopologicalSpaceProd	—	—	Filter.Eventually.mono Filter.Eventually.curry nhds_prod_eq prod_nhdsSet_eq_biSup Filter.Eventually.self_of_nhdsSet
exists_clusterPt 📖	mathematical	IsCompact Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.principal	Set Set.instMembership ClusterPt	—	—
exists_clusterPt_of_frequently 📖	mathematical	IsCompact Filter.Frequently Set Set.instMembership	ClusterPt	—	Filter.frequently_mem_iff_neBot inf_le_right ClusterPt.mono inf_le_left
exists_mapClusterPt 📖	mathematical	IsCompact Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.map Filter.principal	Set Set.instMembership MapClusterPt	—	Filter.map_neBot
exists_mapClusterPt_of_frequently 📖	mathematical	IsCompact Filter.Frequently Set Set.instMembership	MapClusterPt	—	exists_clusterPt_of_frequently
finite 📖	mathematical	IsCompact IsDiscrete	Set.Finite	—	Set.finite_coe_iff finite_of_compact_of_discrete isCompact_iff_compactSpace IsDiscrete.to_subtype
finite_of_discrete 📖	mathematical	IsCompact	Set.Finite	—	nhds_discrete elim_nhds_subcover Set.Finite.subset Finset.finite_toSet Finset.set_biUnion_coe Set.biUnion_of_singleton
image 📖	mathematical	IsCompact Continuous	Set.image	—	image_of_continuousOn Continuous.continuousOn
image_of_continuousOn 📖	mathematical	IsCompact ContinuousOn	Set.image	—	Filter.comap_inf_principal_neBot_of_image_mem Filter.le_principal_iff inf_le_right Set.mem_image_of_mem nhdsWithin.eq_1 instAssociativeMin_mathlib instCommutativeMin_mathlib instIdempotentOpMin_mathlib Filter.Tendsto.inf Filter.tendsto_comap Filter.Tendsto.neBot ClusterPt.neBot
induction_on 📖	—	IsCompact Set Set.instEmptyCollection Set.instUnion Filter Filter.instMembership nhdsWithin	—	—	compl_mem_sets_of_nhdsWithin compl_compl
inf_nhdsSet_eq_biSup 📖	mathematical	IsCompact	Filter Filter.instInf nhdsSet iSup Filter.instSupSet Set Set.instMembership nhds	—	inf_comm nhdsSet_inf_eq_biSup iSup_congr_Prop
insert 📖	mathematical	IsCompact	Set Set.instInsert	—	union isCompact_singleton
inter_iInter_nonempty 📖	—	IsCompact IsClosed Set.Nonempty Set Set.instInter Set.iInter Finset Finset.instMembership	—	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq elim_finite_subfamily_closed
inter_left 📖	mathematical	IsCompact	Set Set.instInter	—	inter_right Set.inter_comm
inter_right 📖	mathematical	IsCompact	Set Set.instInter	—	le_trans Filter.le_principal_iff Set.inter_subset_left IsClosed.mem_of_nhdsWithin_neBot ClusterPt.mono Set.inter_subset_right
le_nhds_of_unique_clusterPt 📖	mathematical	IsCompact Set Filter Filter.instMembership	Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds	—	Filter.le_iff_ultrafilter ultrafilter_le_nhds' ClusterPt.mono ClusterPt.of_le_nhds Ultrafilter.neBot
mem_inf_nhdsSet_of_forall 📖	mathematical	IsCompact Set Filter Filter.instMembership Filter.instInf nhds	nhdsSet	—	inf_nhdsSet_eq_biSup
mem_nhdsSet_inf_of_forall 📖	mathematical	IsCompact Set Filter Filter.instMembership Filter.instInf nhds	nhdsSet	—	nhdsSet_inf_eq_biSup
mem_nhdsSet_prod_of_forall 📖	mathematical	IsCompact Set Filter Filter.instMembership SProd.sprod Filter.instSProd nhds	nhdsSet	—	induction_on nhdsSet_empty Filter.bot_prod Filter.prod_mono nhdsSet_mono le_rfl nhdsSet_union Filter.sup_prod Filter.HasBasis.mem_iff Filter.HasBasis.prod nhds_basis_opens Filter.basis_sets nhdsWithin_le_nhds IsOpen.mem_nhds Filter.mem_of_superset Filter.prod_mem_prod IsOpen.mem_nhdsSet Set.Subset.rfl
mem_prod_nhdsSet_of_forall 📖	mathematical	IsCompact Set Filter Filter.instMembership SProd.sprod Filter.instSProd nhds	nhdsSet	—	prod_nhdsSet_eq_biSup
ne_univ 📖	—	IsCompact	—	—	noncompact_univ
nhdsSetWithin_prod_eq 📖	mathematical	IsCompact	nhdsSetWithin instTopologicalSpaceProd SProd.sprod Set Set.instSProd Filter Filter.instSProd	—	nhdsSet_prod_eq Filter.prod_principal_principal
nhdsSet_inf_eq_biSup 📖	mathematical	IsCompact	Filter Filter.instInf nhdsSet iSup Filter.instSupSet Set Set.instMembership nhds	—	Filter.comap_prod Filter.comap_id iSup_congr_Prop nhdsSet_prod_eq_biSup
nhdsSet_prod_eq 📖	mathematical	IsCompact	nhdsSet instTopologicalSpaceProd SProd.sprod Set Set.instSProd Filter Filter.instSProd	—	nhdsSet_prod_eq_biSup iSup_congr_Prop prod_nhdsSet_eq_biSup sSup_image biSup_prod nhds_prod_eq
nhdsSet_prod_eq_biSup 📖	mathematical	IsCompact	SProd.sprod Filter Filter.instSProd nhdsSet iSup Filter.instSupSet Set Set.instMembership nhds	—	le_antisymm mem_nhdsSet_prod_of_forall iSup₂_le Filter.prod_mono nhds_le_nhdsSet le_rfl
nonempty_iInter_of_directed_nonempty_isCompact_isClosed 📖	mathematical	Directed Set Set.instHasSubset Set.Nonempty IsCompact IsClosed	Set.iInter	—	elim_directed_family_closed Set.Nonempty.mono Set.subset_inter Set.inter_eq_right Set.iInter_subset
nonempty_iInter_of_sequence_nonempty_isCompact_isClosed 📖	mathematical	Set Set.instHasSubset Set.Nonempty IsCompact IsClosed	Set.iInter	—	antitone_nat_of_succ_le Antitone.directed_ge SemilatticeSup.instIsDirectedOrder of_isClosed_subset nonempty_iInter_of_directed_nonempty_isCompact_isClosed
nonempty_sInter_of_directed_nonempty_isCompact_isClosed 📖	mathematical	DirectedOn Set Set.instHasSubset Set.Nonempty IsCompact IsClosed	Set.sInter	—	Set.sInter_eq_iInter nonempty_iInter_of_directed_nonempty_isCompact_isClosed DirectedOn.directed_val
of_isClosed_subset 📖	—	IsCompact Set Set.instHasSubset	—	—	inter_right Set.inter_eq_self_of_subset_right
prod 📖	mathematical	IsCompact	instTopologicalSpaceProd SProd.sprod Set Set.instSProd	—	isCompact_iff_ultrafilter_le_nhds' Filter.mem_map Filter.mem_of_superset nhds_prod_eq le_inf Filter.map_le_iff_le_comap
prod_nhdsSet_eq_biSup 📖	mathematical	IsCompact	SProd.sprod Filter Filter.instSProd nhdsSet iSup Filter.instSupSet Set Set.instMembership nhds	—	Filter.prod_comm nhdsSet_prod_eq_biSup Filter.map_iSup iSup_congr_Prop
sigma_exists_finite_sigma_eq 📖	mathematical	IsCompact instTopologicalSpaceSigma	Set.Finite Set.sigma	—	elim_finite_subcover isOpenMap_sigmaMk IsOpen.preimage continuous_sigmaMk isOpen_univ Set.image_univ Set.range_sigmaMk Finset.finite_toSet Topology.IsClosedEmbedding.isCompact_preimage Topology.IsClosedEmbedding.sigmaMk Set.ext Set.mem_iUnion Set.iUnion_congr_Prop Sigma.eta
tendsto_nhds_of_unique_mapClusterPt 📖	mathematical	IsCompact Filter.Eventually Set Set.instMembership	Filter.Tendsto nhds	—	le_nhds_of_unique_clusterPt Filter.mem_map
ultrafilter_le_nhds 📖	mathematical	IsCompact Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Ultrafilter.toFilter Filter.principal	Set Set.instMembership nhds	—	isCompact_iff_ultrafilter_le_nhds
ultrafilter_le_nhds' 📖	mathematical	IsCompact Set Ultrafilter Ultrafilter.instMembershipSet	Set.instMembership Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Ultrafilter.toFilter nhds	—	isCompact_iff_ultrafilter_le_nhds'
union 📖	mathematical	IsCompact	Set Set.instUnion	—	Set.union_eq_iUnion isCompact_iUnion Bool.instFinite

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace 📖	mathematical	CompactSpace	topologicalSpace	—	Set.pi_univ isCompact_univ_pi isCompact_univ
exists_compact_superset_iff 📖	mathematical	—	IsCompact topologicalSpace Set Set.instHasSubset Set.preimage Function.eval	—	IsCompact.image continuous_apply HasSubset.Subset.trans Set.instIsTransSubset Set.subset_preimage_image isCompact_univ_pi
isCompact_iff_of_isClosed 📖	mathematical	—	IsCompact topologicalSpace Set.image Function.eval	—	IsCompact.image continuous_apply IsCompact.of_isClosed_subset isCompact_univ_pi Set.subset_pi_eval_image

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
noncompactSpace_iff 📖	mathematical	—	NoncompactSpace instTopologicalSpaceProd	—	—
noncompactSpace_left 📖	mathematical	—	NoncompactSpace instTopologicalSpaceProd	—	noncompactSpace_iff
noncompactSpace_right 📖	mathematical	—	NoncompactSpace instTopologicalSpaceProd	—	noncompactSpace_iff

Quot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace 📖	mathematical	—	CompactSpace instTopologicalSpaceQuot	—	isCompact_range

Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace 📖	mathematical	—	CompactSpace instTopologicalSpaceQuotient	—	Quot.compactSpace

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact_sigma 📖	mathematical	IsCompact	instTopologicalSpaceSigma sigma	—	sigma_eq_biUnion Finite.isCompact_biUnion IsCompact.image continuous_sigmaMk
sUnion_isCompact_eq_univ 📖	mathematical	—	sUnion setOf Set IsCompact univ	—	eq_univ_of_forall

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact 📖	mathematical	—	IsCompact	—	isCompact_biUnion isCompact_singleton Set.biUnion_of_singleton
isCompact_biUnion 📖	mathematical	IsCompact	Set.iUnion Set Set.instMembership	—	isCompact_iff_ultrafilter_le_nhds' Ultrafilter.finite_biUnion_mem_iff IsCompact.ultrafilter_le_nhds Filter.le_principal_iff Set.mem_iUnion₂
isCompact_sUnion 📖	mathematical	IsCompact	Set.sUnion	—	Set.sUnion_eq_biUnion isCompact_biUnion

Set.Infinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_accPt_cofinite_inf_principal 📖	mathematical	Set.Infinite	AccPt Filter Filter.instInf Filter.cofinite Filter.principal	—	exists_accPt_cofinite_inf_principal_of_subset_isCompact isCompact_univ Set.subset_univ
exists_accPt_cofinite_inf_principal_of_subset_isCompact 📖	mathematical	Set.Infinite IsCompact Set Set.instHasSubset	Set.instMembership AccPt Filter Filter.instInf Filter.cofinite Filter.principal	—	accPt_iff_clusterPt inf_comm inf_right_comm Set.Finite.cofinite_inf_principal_compl Set.finite_singleton cofinite_inf_principal_neBot LE.le.trans inf_le_right Filter.principal_mono
exists_accPt_of_subset_isCompact 📖	mathematical	Set.Infinite IsCompact Set Set.instHasSubset	Set.instMembership AccPt Filter.principal	—	exists_accPt_cofinite_inf_principal_of_subset_isCompact AccPt.mono inf_le_right
exists_accPt_principal 📖	mathematical	Set.Infinite	AccPt Filter.principal	—	AccPt.mono inf_le_right exists_accPt_cofinite_inf_principal

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact 📖	mathematical	Set.Subsingleton	IsCompact	—	induction_on isCompact_empty isCompact_singleton

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace 📖	mathematical	—	CompactSpace	—	Set.Subsingleton.isCompact Set.subsingleton_univ

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact_iff 📖	mathematical	—	IsCompact instTopologicalSpaceSubtype Set.image	—	Topology.IsEmbedding.isCompact_iff Topology.IsEmbedding.subtypeVal

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace 📖	mathematical	Topology.IsClosedEmbedding	CompactSpace	—	Topology.IsInducing.isCompact_iff isInducing Set.image_univ IsClosed.isCompact isClosed_range
isCompact_preimage 📖	mathematical	Topology.IsClosedEmbedding IsCompact	Set.preimage	—	Topology.IsInducing.isCompact_preimage isInducing isClosed_range
noncompactSpace 📖	mathematical	Topology.IsClosedEmbedding	NoncompactSpace	—	noncompactSpace_of_neBot Filter.Tendsto.neBot tendsto_cocompact instNeBotCocompactOfNoncompactSpace
tendsto_cocompact 📖	mathematical	Topology.IsClosedEmbedding	Filter.Tendsto Filter.cocompact	—	Filter.HasBasis.tendsto_right_iff Filter.hasBasis_cocompact IsCompact.compl_mem_cocompact isCompact_preimage

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact_iff 📖	mathematical	Topology.IsEmbedding	IsCompact Set.image	—	Topology.IsInducing.isCompact_iff isInducing

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact_iff 📖	mathematical	Topology.IsInducing	IsCompact Set.image	—	IsCompact.image continuous Filter.map_neBot LE.le.trans_eq Filter.map_mono Filter.map_principal mapClusterPt_iff
isCompact_preimage 📖	mathematical	Topology.IsInducing IsCompact	Set.preimage	—	IsCompact.inter_right isCompact_iff Set.image_preimage_eq_inter_range
isCompact_preimage' 📖	mathematical	Topology.IsInducing IsCompact Set Set.instHasSubset Set.range	Set.preimage	—	isCompact_preimage_iff
isCompact_preimage_iff 📖	mathematical	Topology.IsInducing Set Set.instHasSubset Set.range	IsCompact Set.preimage	—	isCompact_iff Set.image_preimage_eq_of_subset

ULift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace 📖	mathematical	—	CompactSpace topologicalSpace	—	Topology.IsClosedEmbedding.compactSpace Topology.IsClosedEmbedding.uliftDown

Ultrafilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_nhds_lim 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder toFilter nhds lim	—	IsCompact.ultrafilter_le_nhds isCompact_univ Filter.principal_univ le_nhds_lim

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace_generateFrom 📖	mathematical	TopologicalSpace.generateFrom Set Set.instHasSubset Set.Finite Set.sUnion Set.univ	CompactSpace	—	isCompact_univ_iff isCompact_generateFrom
compactSpace_generateFrom' 📖	mathematical	TopologicalSpace.generateFrom Set.Finite Set.iUnion Set Set.instMembership Set.univ	CompactSpace	—	isCompact_univ_iff isCompact_generateFrom'
compactSpace_of_finite_subfamily_closed 📖	mathematical	Set.iInter Finset Finset.instMembership Set Set.instEmptyCollection	CompactSpace	—	isCompact_of_finite_subfamily_closed Set.univ_inter
disjoint_map_cocompact 📖	mathematical	Continuous Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter Filter.cocompact	Filter.map	—	Filter.disjoint_comap_iff_map disjoint_iff_inf_le inf_le_inf_left Filter.comap_cocompact_le disjoint_iff
exists_clusterPt_of_compactSpace 📖	mathematical	—	ClusterPt	—	isCompact_univ Filter.principal_univ
exists_nhds_ne_inf_principal_neBot 📖	mathematical	IsCompact Set.Infinite	Set Set.instMembership Filter.NeBot Filter Filter.instInf nhdsWithin Compl.compl Set.instCompl Set.instSingletonSet Filter.principal	—	Set.Infinite.exists_accPt_of_subset_isCompact Set.Subset.rfl
exists_nhds_ne_neBot 📖	mathematical	—	Filter.NeBot nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	—	Filter.principal_univ inf_of_le_left Set.Infinite.exists_accPt_principal Set.infinite_univ
exists_subset_nhds_of_compactSpace 📖	—	Directed Set Set.instHasSubset IsClosed Filter Filter.instMembership nhds	—	—	exists_subset_nhds_of_isCompact' IsClosed.isCompact
exists_subset_nhds_of_isCompact' 📖	—	Directed Set Set.instHasSubset IsCompact IsClosed Filter Filter.instMembership nhds	—	—	exists_open_set_nhds Set.inter_compl_nonempty_iff IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed IsCompact.inter_right IsOpen.isClosed_compl IsClosed.inter HasSubset.Subset.trans Set.instIsTransSubset
finite_cover_nhds 📖	mathematical	Set Filter Filter.instMembership nhds	Set.iUnion Finset Finset.instMembership Set.univ	—	finite_cover_nhds_interior Set.univ_subset_iff HasSubset.Subset.trans Set.instIsTransSubset Eq.subset Set.instReflSubset Set.iUnion₂_mono interior_subset
finite_cover_nhds_interior 📖	mathematical	Set Filter Filter.instMembership nhds	Set.iUnion Finset Finset.instMembership interior Set.univ	—	IsCompact.elim_finite_subcover isCompact_univ isOpen_interior Set.mem_iUnion mem_interior_iff_mem_nhds Set.univ_subset_iff
finite_of_compact_of_discrete 📖	mathematical	—	Finite	—	Finite.of_finite_univ IsCompact.finite_of_discrete isCompact_univ
generalized_tube_lemma 📖	—	IsCompact IsOpen instTopologicalSpaceProd Set Set.instHasSubset SProd.sprod Set.instSProd	—	—	Filter.HasBasis.mem_iff Filter.HasBasis.prod hasBasis_nhdsSet IsCompact.nhdsSet_prod_eq IsOpen.mem_nhdsSet
generalized_tube_lemma' 📖	mathematical	IsCompact Set Filter Filter.instMembership nhdsSetWithin instTopologicalSpaceProd SProd.sprod Set.instSProd	Set.instHasSubset	—	Filter.mem_prod_iff IsCompact.nhdsSetWithin_prod_eq
generalized_tube_lemma_left 📖	mathematical	IsCompact Set Filter Filter.instMembership nhdsSetWithin instTopologicalSpaceProd SProd.sprod Set.instSProd	Set.instHasSubset	—	Filter.mem_prod_principal nhdsSetWithin_self IsCompact.nhdsSetWithin_prod_eq
generalized_tube_lemma_right 📖	mathematical	IsCompact Set Filter Filter.instMembership nhdsSetWithin instTopologicalSpaceProd SProd.sprod Set.instSProd	Set.instHasSubset	—	Filter.mem_prod_iff nhdsSetWithin_self IsCompact.nhdsSetWithin_prod_eq HasSubset.Subset.trans Set.instIsTransSubset Set.prod_mono_left
instCompactSpaceProd 📖	mathematical	—	CompactSpace instTopologicalSpaceProd	—	Set.univ_prod_univ IsCompact.prod isCompact_univ
instCompactSpaceSigmaOfFinite 📖	mathematical	CompactSpace	instTopologicalSpaceSigma	—	Set.Sigma.univ isCompact_iUnion isCompact_range continuous_sigmaMk
instCompactSpaceSum 📖	mathematical	—	CompactSpace instTopologicalSpaceSum	—	Set.range_inl_union_range_inr IsCompact.union isCompact_range continuous_inl continuous_inr
instNeBotCoclosedCompactOfNoncompactSpace 📖	mathematical	—	Filter.NeBot Filter.coclosedCompact	—	Filter.neBot_of_le instNeBotCocompactOfNoncompactSpace Filter.cocompact_le_coclosedCompact
instNeBotCocompactOfNoncompactSpace 📖	mathematical	—	Filter.NeBot Filter.cocompact	—	Filter.HasBasis.neBot_iff Filter.hasBasis_cocompact Mathlib.Tactic.Contrapose.contrapose₁ Set.compl_empty_iff Set.not_nonempty_iff_eq_empty noncompact_univ
instNoncompactSpaceInt 📖	mathematical	—	NoncompactSpace instTopologicalSpaceInt	—	noncompactSpace_of_neBot Filter.cocompact_eq_cofinite instDiscreteTopologyInt Int.infinite
isCompact_accumulate 📖	mathematical	IsCompact	Set.accumulate	—	Set.Finite.isCompact_biUnion Set.finite_le_nat
isCompact_diagonal 📖	mathematical	—	IsCompact instTopologicalSpaceProd Set.diagonal	—	isCompact_range Continuous.prodMk continuous_id Set.range_diag
isCompact_empty 📖	mathematical	—	IsCompact Set Set.instEmptyCollection	—	Filter.NeBot.ne Filter.empty_mem_iff_bot Filter.le_principal_iff
isCompact_generateFrom 📖	mathematical	TopologicalSpace.generateFrom Set Set.instHasSubset Set.Finite Set.sUnion	IsCompact	—	isCompact_iff_ultrafilter_le_nhds' TopologicalSpace.nhds_generateFrom Set.mem_sUnion_of_mem Set.sInter_image Filter.biInter_mem Ultrafilter.compl_mem_iff_notMem Filter.mem_of_superset Function.sometimes_spec
isCompact_generateFrom' 📖	mathematical	TopologicalSpace.generateFrom Set.Finite Set Set.instHasSubset Set.iUnion Set.instMembership	IsCompact	—	isCompact_generateFrom Set.sUnion_eq_iUnion Subtype.coe_preimage_self Set.Finite.image Set.sUnion_image Set.iUnion_coe_set Set.iUnion_congr_Prop
isCompact_iUnion 📖	mathematical	IsCompact	Set.iUnion	—	Set.Finite.isCompact_sUnion Set.finite_range Set.forall_mem_range
isCompact_iff_compactSpace 📖	mathematical	—	IsCompact CompactSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	isCompact_iff_isCompact_univ isCompact_univ_iff
isCompact_iff_finite 📖	mathematical	—	IsCompact Set.Finite	—	IsCompact.finite_of_discrete Set.Finite.isCompact
isCompact_iff_finite_subcover 📖	mathematical	—	IsCompact Set Set.instHasSubset Set.iUnion Finset Finset.instMembership	—	IsCompact.elim_finite_subcover isCompact_of_finite_subcover
isCompact_iff_finite_subfamily_closed 📖	mathematical	—	IsCompact Set Set.instInter Set.iInter Finset Finset.instMembership Set.instEmptyCollection	—	IsCompact.elim_finite_subfamily_closed isCompact_of_finite_subfamily_closed
isCompact_iff_isCompact_univ 📖	mathematical	—	IsCompact Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.univ	—	Subtype.isCompact_iff Set.image_univ Subtype.range_coe
isCompact_iff_ultrafilter_le_nhds 📖	mathematical	—	IsCompact Set Set.instMembership Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Ultrafilter.toFilter nhds	—	Filter.forall_neBot_le_iff ClusterPt.mono
isCompact_iff_ultrafilter_le_nhds' 📖	mathematical	—	IsCompact Set Set.instMembership Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Ultrafilter.toFilter nhds	—	—
isCompact_of_finite_subcover 📖	mathematical	Set Set.instHasSubset Set.iUnion Finset Finset.instMembership	IsCompact	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq Mathlib.Tactic.Push.not_forall_eq Set.mem_iUnion Filter.compl_notMem Filter.le_principal_iff Filter.mem_of_superset Filter.biInter_finset_mem Set.subset_compl_comm Set.compl_iInter₂ Set.iUnion_congr_Prop compl_compl Filter.HasBasis.disjoint_iff_left nhds_basis_opens
isCompact_of_finite_subfamily_closed 📖	mathematical	Set Set.instInter Set.iInter Finset Finset.instMembership Set.instEmptyCollection	IsCompact	—	isCompact_of_finite_subcover IsOpen.isClosed_compl disjoint_iff Set.compl_iUnion Set.disjoint_compl_right_iff_subset Set.compl_iUnion₂
isCompact_pi_infinite 📖	mathematical	IsCompact	Pi.topologicalSpace setOf	—	nhds_pi Filter.mem_map Filter.mem_of_superset
isCompact_range 📖	mathematical	Continuous	IsCompact Set.range	—	Set.image_univ IsCompact.image isCompact_univ
isCompact_singleton 📖	mathematical	—	IsCompact Set Set.instSingletonSet	—	ClusterPt.of_le_nhds' LE.le.trans Filter.principal_singleton pure_le_nhds
isCompact_univ 📖	mathematical	—	IsCompact Set.univ	—	CompactSpace.isCompact_univ
isCompact_univ_iff 📖	mathematical	—	IsCompact Set.univ CompactSpace	—	CompactSpace.isCompact_univ
isCompact_univ_pi 📖	mathematical	IsCompact	Pi.topologicalSpace Set.pi Set.univ	—	isCompact_pi_infinite
le_nhds_of_unique_clusterPt 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds	—	IsCompact.le_nhds_of_unique_clusterPt isCompact_univ Filter.univ_mem
nhdsSet_prod_le_of_disjoint_cocompact 📖	mathematical	IsCompact Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter Filter.cocompact	SProd.sprod Filter.instSProd nhdsSet instTopologicalSpaceProd Set Set.instSProd Set.univ	—	Filter.disjoint_cocompact_right Filter.prod_mono_right Filter.le_principal_iff principal_le_nhdsSet IsCompact.nhdsSet_prod_eq nhdsSet_mono Set.prod_mono_right le_top
nhds_prod_le_of_disjoint_cocompact 📖	mathematical	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter Filter.cocompact	SProd.sprod Filter.instSProd nhds nhdsSet instTopologicalSpaceProd Set Set.instSProd Set.instSingletonSet Set.univ	—	nhdsSet_singleton nhdsSet_prod_le_of_disjoint_cocompact isCompact_singleton
noncompactSpace_of_neBot 📖	mathematical	—	NoncompactSpace	—	Set.Nonempty.ne_empty Filter.nonempty_of_mem IsCompact.compl_mem_cocompact Set.compl_univ
noncompact_univ 📖	mathematical	—	IsCompact Set.univ	—	NoncompactSpace.noncompact_univ
not_compactSpace_iff 📖	mathematical	—	CompactSpace NoncompactSpace	—	—
prod_nhdsSet_le_of_disjoint_cocompact 📖	mathematical	IsCompact Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter Filter.cocompact	SProd.sprod Filter.instSProd nhdsSet instTopologicalSpaceProd Set Set.instSProd Set.univ	—	Filter.disjoint_cocompact_right Filter.prod_mono_left Filter.le_principal_iff principal_le_nhdsSet IsCompact.nhdsSet_prod_eq nhdsSet_mono Set.prod_mono_left le_top
prod_nhds_le_of_disjoint_cocompact 📖	mathematical	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter Filter.cocompact	SProd.sprod Filter.instSProd nhds nhdsSet instTopologicalSpaceProd Set Set.instSProd Set.univ Set.instSingletonSet	—	nhdsSet_singleton prod_nhdsSet_le_of_disjoint_cocompact isCompact_singleton
tendsto_nhds_of_unique_mapClusterPt 📖	mathematical	—	Filter.Tendsto nhds	—	le_nhds_of_unique_clusterPt

---

← Back to Index