SigmaCompact

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

Statistics

Metric	Count
Definitions CompactExhaustion, choice, find, instFunLikeNatSet, instInhabitedOfSigmaCompactSpaceOfWeaklyLocallyCompactSpace, shiftr, toFun, IsSigmaCompact, encodable, SigmaCompactSpace, compactCovering	11
Theorems exists_mem, exists_mem_nhds, exists_superset_of_isCompact, find_shiftr, iUnion_eq, iUnion_eq', instRelHomClassNatSetLeSubset, isCompact, isCompact', mem_diff_shiftr_find, mem_find, mem_iff_find_le, subset, subset_interior, subset_interior_succ, subset_interior_succ', subset_succ, toFun_eq_coe, sigmaCompact, sigmaCompactSpace, isSigmaCompact, image, image_of_continuousOn, of_isClosed_subset, countable_univ, exists_compact_covering, isSigmaCompact_univ, of_countable, SigmaCompactSpace_iff_exists_compact_covering, isSigmaCompact_iff, sigmaCompactSpace, isSigmaCompact_iff, isSigmaCompact_iff, compactCovering_subset, countable_cover_nhdsWithin_of_sigmaCompact, countable_cover_nhds_of_sigmaCompact, exists_mem_compactCovering, iUnion_closure_compactCovering, iUnion_compactCovering, instSigmaCompactSpaceForallOfFinite, instSigmaCompactSpaceProd, instSigmaCompactSpaceSigmaOfCountable, instSigmaCompactSpaceSum, instSigmaCompactSpaceULift, isCompact_compactCovering, isSigmaCompact_biUnion, isSigmaCompact_empty, isSigmaCompact_iUnion, isSigmaCompact_iUnion_of_isCompact, isSigmaCompact_iff_isSigmaCompact_univ, isSigmaCompact_iff_sigmaCompactSpace, isSigmaCompact_range, isSigmaCompact_sUnion, isSigmaCompact_sUnion_of_isCompact, isSigmaCompact_univ, isSigmaCompact_univ_iff, sigmaCompactSpace_of_locallyCompact_secondCountable	57
Total	68

CompactExhaustion

Definitions

Name	Category	Theorems
choice 📖	CompOp	—
find 📖	CompOp	4 math math: find_shiftr, mem_find, mem_diff_shiftr_find, mem_iff_find_le
instFunLikeNatSet 📖	CompOp	15 math math: isClosed, exists_mem, mem_find, instRelHomClassNatSetLeSubset, subset, exists_mem_nhds, iUnion_eq, isCompact, subset_interior, subset_succ, subset_interior_succ, exists_superset_of_isCompact, mem_diff_shiftr_find, toFun_eq_coe, mem_iff_find_le
instInhabitedOfSigmaCompactSpaceOfWeaklyLocallyCompactSpace 📖	CompOp	—
shiftr 📖	CompOp	2 math math: find_shiftr, mem_diff_shiftr_find
toFun 📖	CompOp	4 math math: subset_interior_succ', isCompact', iUnion_eq', toFun_eq_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_mem 📖	mathematical	—	Set Set.instMembership DFunLike.coe CompactExhaustion instFunLikeNatSet	—	Set.iUnion_eq_univ_iff iUnion_eq
exists_mem_nhds 📖	mathematical	—	Set Filter Filter.instMembership nhds DFunLike.coe CompactExhaustion instFunLikeNatSet	—	exists_mem mem_interior_iff_mem_nhds subset_interior_succ
exists_superset_of_isCompact 📖	mathematical	IsCompact	Set Set.instHasSubset DFunLike.coe CompactExhaustion instFunLikeNatSet	—	IsCompact.elim_directed_cover isOpen_interior exists_mem Set.mem_iUnion subset_interior_succ Monotone.directed_le SemilatticeSup.instIsDirectedOrder interior_mono subset Set.Subset.trans interior_subset
find_shiftr 📖	mathematical	—	find shiftr	—	Nat.find_comp_succ exists_mem Set.notMem_empty
iUnion_eq 📖	mathematical	—	Set.iUnion DFunLike.coe CompactExhaustion Set instFunLikeNatSet Set.univ	—	iUnion_eq'
iUnion_eq' 📖	mathematical	—	Set.iUnion toFun Set.univ	—	—
instRelHomClassNatSetLeSubset 📖	mathematical	—	RelHomClass CompactExhaustion Set Set.instHasSubset instFunLikeNatSet	—	monotone_nat_of_le_succ HasSubset.Subset.trans Set.instIsTransSubset subset_interior_succ' interior_subset
isCompact 📖	mathematical	—	IsCompact DFunLike.coe CompactExhaustion Set instFunLikeNatSet	—	isCompact'
isCompact' 📖	mathematical	—	IsCompact toFun	—	—
mem_diff_shiftr_find 📖	mathematical	—	Set Set.instMembership Set.instSDiff DFunLike.coe CompactExhaustion instFunLikeNatSet shiftr find	—	mem_find mem_iff_find_le find_shiftr
mem_find 📖	mathematical	—	Set Set.instMembership DFunLike.coe CompactExhaustion instFunLikeNatSet find	—	Nat.find_spec exists_mem
mem_iff_find_le 📖	mathematical	—	Set Set.instMembership DFunLike.coe CompactExhaustion instFunLikeNatSet find	—	Nat.find_min' exists_mem subset mem_find
subset 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe CompactExhaustion instFunLikeNatSet	—	OrderHomClass.mono instRelHomClassNatSetLeSubset
subset_interior 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe CompactExhaustion instFunLikeNatSet interior	—	Set.Subset.trans subset_interior_succ interior_mono subset
subset_interior_succ 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe CompactExhaustion instFunLikeNatSet interior	—	subset_interior_succ'
subset_interior_succ' 📖	mathematical	—	Set Set.instHasSubset toFun interior	—	—
subset_succ 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe CompactExhaustion instFunLikeNatSet	—	subset
toFun_eq_coe 📖	mathematical	—	toFun DFunLike.coe CompactExhaustion Set instFunLikeNatSet	—	—

CompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sigmaCompact 📖	mathematical	—	SigmaCompactSpace	—	isCompact_univ Set.iUnion_const

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sigmaCompactSpace 📖	mathematical	—	SigmaCompactSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	Topology.IsClosedEmbedding.sigmaCompactSpace isClosedEmbedding_subtypeVal

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSigmaCompact 📖	mathematical	IsCompact	IsSigmaCompact	—	Set.iUnion_const

IsSigmaCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image 📖	mathematical	Continuous IsSigmaCompact	Set.image	—	image_of_continuousOn Continuous.continuousOn
image_of_continuousOn 📖	mathematical	IsSigmaCompact ContinuousOn	Set.image	—	IsCompact.image_of_continuousOn ContinuousOn.mono Set.subset_iUnion Set.image_iUnion
of_isClosed_subset 📖	—	IsSigmaCompact Set Set.instHasSubset	—	—	IsCompact.inter_left Set.inter_iUnion Set.inter_eq_left

LocallyFinite

Definitions

Name	Category	Theorems
encodable 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable_univ 📖	mathematical	LocallyFinite Set.Nonempty	Set.Countable Set.univ	—	finite_nonempty_inter_compact isCompact_compactCovering Set.Countable.mono Set.iUnion_eq_univ_iff iUnion_compactCovering Set.mem_iUnion Set.countable_iUnion instCountableNat Set.Finite.countable

SigmaCompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_compact_covering 📖	mathematical	—	IsCompact Set.iUnion Set.univ	—	SigmaCompactSpace_iff_exists_compact_covering
isSigmaCompact_univ 📖	mathematical	—	IsSigmaCompact Set.univ	—	—
of_countable 📖	mathematical	IsCompact Set.sUnion Set.univ	SigmaCompactSpace	—	Set.exists_seq_cover_iff_countable isCompact_empty

Subtype

Theorems

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

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sigmaCompactSpace 📖	mathematical	Topology.IsClosedEmbedding	SigmaCompactSpace	—	isCompact_preimage isCompact_compactCovering Set.preimage_iUnion iUnion_compactCovering Set.preimage_univ

Topology.IsEmbedding

Theorems

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

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSigmaCompact_iff 📖	mathematical	Topology.IsInducing	IsSigmaCompact Set.image	—	IsSigmaCompact.image continuous Set.image_preimage_inter Set.inter_eq_left HasSubset.Subset.trans Set.instIsTransSubset Set.subset_iUnion Eq.le isCompact_iff Set.preimage_iUnion Set.iUnion_inter Set.inter_eq_right Set.subset_preimage_image

(root)

Definitions

Name	Category	Theorems
CompactExhaustion 📖	CompData	15 math math: CompactExhaustion.isClosed, CompactExhaustion.exists_mem, CompactExhaustion.mem_find, CompactExhaustion.instRelHomClassNatSetLeSubset, CompactExhaustion.subset, CompactExhaustion.exists_mem_nhds, CompactExhaustion.iUnion_eq, CompactExhaustion.isCompact, CompactExhaustion.subset_interior, CompactExhaustion.subset_succ, CompactExhaustion.subset_interior_succ, CompactExhaustion.exists_superset_of_isCompact, CompactExhaustion.mem_diff_shiftr_find, CompactExhaustion.toFun_eq_coe, CompactExhaustion.mem_iff_find_le
IsSigmaCompact 📖	MathDef	15 math math: isSigmaCompact_univ, Topology.IsInducing.isSigmaCompact_iff, isSigmaCompact_iff_isSigmaCompact_univ, SigmaCompactSpace.isSigmaCompact_univ, Topology.IsEmbedding.isSigmaCompact_iff, IsCompact.isSigmaCompact, isSigmaCompact_iUnion_of_isCompact, isSigmaCompact_sUnion_of_isCompact, Homeomorph.isSigmaCompact_image, isSigmaCompact_iff_sigmaCompactSpace, isSigmaCompact_range, Subtype.isSigmaCompact_iff, isSigmaCompact_empty, Homeomorph.isSigmaCompact_preimage, isSigmaCompact_univ_iff
SigmaCompactSpace 📖	CompData	13 math math: sigmaCompactSpace_of_locallyCompact_secondCountable, SeparableWeaklyLocallyCompactGroup.sigmaCompactSpace, SigmaCompactSpace_iff_exists_compact_covering, instSigmaCompactSpaceProd, instSigmaCompactSpaceSum, IsClosed.sigmaCompactSpace, instSigmaCompactSpaceULift, CompactSpace.sigmaCompact, isSigmaCompact_iff_sigmaCompactSpace, SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace, Topology.IsClosedEmbedding.sigmaCompactSpace, isSigmaCompact_univ_iff, SigmaCompactSpace.of_countable
compactCovering 📖	CompOp	5 math math: iUnion_closure_compactCovering, iUnion_compactCovering, isCompact_compactCovering, exists_mem_compactCovering, compactCovering_subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SigmaCompactSpace_iff_exists_compact_covering 📖	mathematical	—	SigmaCompactSpace IsCompact Set.iUnion Set.univ	—	isSigmaCompact_univ_iff IsSigmaCompact.eq_1
compactCovering_subset 📖	mathematical	—	Set Set.instHasSubset compactCovering	—	Set.monotone_accumulate SigmaCompactSpace.exists_compact_covering
countable_cover_nhdsWithin_of_sigmaCompact 📖	mathematical	Set Filter Filter.instMembership nhdsWithin	Set.instHasSubset Set.Countable Set.iUnion Set.instMembership	—	Set.iUnion_subset Set.countable_iUnion instCountableNat Finset.countable_toSet Set.mem_iUnion₂ exists_mem_compactCovering Set.mem_iUnion IsCompact.elim_nhds_subcover IsCompact.inter_right isCompact_compactCovering
countable_cover_nhds_of_sigmaCompact 📖	mathematical	Set Filter Filter.instMembership nhds	Set.Countable Set.iUnion Set.instMembership Set.univ	—	countable_cover_nhdsWithin_of_sigmaCompact isClosed_univ Set.univ_subset_iff
exists_mem_compactCovering 📖	mathematical	—	Set Set.instMembership compactCovering	—	Set.iUnion_eq_univ_iff iUnion_compactCovering
iUnion_closure_compactCovering 📖	mathematical	—	Set.iUnion closure compactCovering Set.univ	—	eq_top_mono Set.iUnion_mono subset_closure iUnion_compactCovering
iUnion_compactCovering 📖	mathematical	—	Set.iUnion compactCovering Set.univ	—	SigmaCompactSpace.exists_compact_covering compactCovering.eq_1 Set.iUnion_accumulate
instSigmaCompactSpaceForallOfFinite 📖	mathematical	SigmaCompactSpace	Pi.topologicalSpace	—	isCompact_univ_pi isCompact_compactCovering Set.iUnion_univ_pi_of_monotone compactCovering_subset iUnion_compactCovering Set.pi_univ
instSigmaCompactSpaceProd 📖	mathematical	—	SigmaCompactSpace instTopologicalSpaceProd	—	IsCompact.prod isCompact_compactCovering Set.iUnion_prod_of_monotone compactCovering_subset iUnion_compactCovering Set.univ_prod_univ
instSigmaCompactSpaceSigmaOfCountable 📖	mathematical	SigmaCompactSpace	instTopologicalSpaceSigma	—	isEmpty_or_nonempty CompactSpace.sigmaCompact Finite.compactSpace Finite.of_subsingleton IsEmpty.instSubsingleton Sigma.isEmpty_left exists_surjective_nat Set.Finite.isCompact_biUnion Set.finite_le_nat IsCompact.image isCompact_compactCovering continuous_sigmaMk Function.Surjective.forall exists_mem_compactCovering le_max_left Set.mem_image_of_mem compactCovering_subset le_max_right
instSigmaCompactSpaceSum 📖	mathematical	—	SigmaCompactSpace instTopologicalSpaceSum	—	IsCompact.union IsCompact.image isCompact_compactCovering continuous_inl continuous_inr Set.iUnion_union_distrib iUnion_compactCovering Set.image_univ Set.range_inl_union_range_inr
instSigmaCompactSpaceULift 📖	mathematical	—	SigmaCompactSpace ULift.topologicalSpace	—	Topology.IsClosedEmbedding.sigmaCompactSpace Topology.IsClosedEmbedding.uliftDown
isCompact_compactCovering 📖	mathematical	—	IsCompact compactCovering	—	isCompact_accumulate SigmaCompactSpace.exists_compact_covering
isSigmaCompact_biUnion 📖	mathematical	IsSigmaCompact	Set.iUnion Set Set.instMembership	—	Set.countable_coe_iff Set.biUnion_eq_iUnion isSigmaCompact_iUnion
isSigmaCompact_empty 📖	mathematical	—	IsSigmaCompact Set Set.instEmptyCollection	—	IsCompact.isSigmaCompact isCompact_empty
isSigmaCompact_iUnion 📖	mathematical	IsSigmaCompact	Set.iUnion	—	Function.uncurry_def Set.iUnion_prod' isSigmaCompact_iUnion_of_isCompact instCountableProd instCountableNat
isSigmaCompact_iUnion_of_isCompact 📖	mathematical	IsCompact	IsSigmaCompact Set.iUnion	—	isEmpty_or_nonempty Set.iUnion_of_empty countable_iff_exists_surjective Function.Surjective.iUnion_comp
isSigmaCompact_iff_isSigmaCompact_univ 📖	mathematical	—	IsSigmaCompact Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.univ	—	Subtype.isSigmaCompact_iff Set.image_univ Subtype.range_coe
isSigmaCompact_iff_sigmaCompactSpace 📖	mathematical	—	IsSigmaCompact SigmaCompactSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	isSigmaCompact_iff_isSigmaCompact_univ isSigmaCompact_univ_iff
isSigmaCompact_range 📖	mathematical	Continuous	IsSigmaCompact Set.range	—	IsSigmaCompact.image isSigmaCompact_univ Set.image_univ
isSigmaCompact_sUnion 📖	mathematical	IsSigmaCompact Set Set.instMembership	Set.sUnion	—	Set.countable_coe_iff isSigmaCompact_iUnion Set.sUnion_eq_iUnion
isSigmaCompact_sUnion_of_isCompact 📖	mathematical	IsCompact	IsSigmaCompact Set.sUnion	—	Set.countable_coe_iff Set.sUnion_eq_iUnion isSigmaCompact_iUnion_of_isCompact
isSigmaCompact_univ 📖	mathematical	—	IsSigmaCompact Set.univ	—	isSigmaCompact_univ_iff
isSigmaCompact_univ_iff 📖	mathematical	—	IsSigmaCompact Set.univ SigmaCompactSpace	—	SigmaCompactSpace.isSigmaCompact_univ
sigmaCompactSpace_of_locallyCompact_secondCountable 📖	mathematical	—	SigmaCompactSpace	—	TopologicalSpace.countable_cover_nhds SigmaCompactSpace.of_countable Set.Countable.image Set.forall_mem_image Set.sUnion_image WeaklyLocallyCompactSpace.exists_compact_mem_nhds instWeaklyLocallyCompactSpaceOfLocallyCompactSpace

---

← Back to Index