LocallyCompact

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

Statistics

Metric	Count
Definitions	0
Theorems locallyCompactSpace, locallyCompactSpace_of_finite, locallyCompactSpace, weaklyLocallyCompactSpace, nhdsSet_basis_isCompact, locallyCompactSpace, locallyCompactSpace, locallyCompactSpace, weaklyLocallyCompactSpace, of_hasBasis, locallyCompactSpace, locallyCompactSpace_of_finite, locallyCompactSpace, locallyCompactSpace, weaklyLocallyCompactSpace, locallyCompactSpace, locallyCompactSpace, compact_basis_nhds, disjoint_nhds_cocompact, exists_compact_between, exists_compact_subset, exists_compact_superset, exists_mem_nhdsSet_isCompact_mapsTo, instLocallyCompactPairOfLocallyCompactSpace, instWeaklyLocallyCompactSpaceForallOfFinite, instWeaklyLocallyCompactSpaceOfCompactSpace, instWeaklyLocallyCompactSpaceOfLocallyCompactSpace, instWeaklyLocallyCompactSpaceProd, local_compact_nhds	29
Total	29

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallyCompactSpace 📖	mathematical	—	LocallyCompactSpace Pi.topologicalSpace	—	Pi.locallyCompactSpace
locallyCompactSpace_of_finite 📖	mathematical	—	LocallyCompactSpace Pi.topologicalSpace	—	Pi.locallyCompactSpace_of_finite

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallyCompactSpace 📖	mathematical	—	LocallyCompactSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	IsLocallyClosed.locallyCompactSpace isLocallyClosed
weaklyLocallyCompactSpace 📖	mathematical	—	WeaklyLocallyCompactSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	Topology.IsClosedEmbedding.weaklyLocallyCompactSpace isClosedEmbedding_subtypeVal

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nhdsSet_basis_isCompact 📖	mathematical	IsCompact	Filter.HasBasis Set nhdsSet Filter Filter.instMembership	—	Filter.hasBasis_self Filter.HasBasis.forall_iff hasBasis_nhdsSet exists_compact_between subset_interior_iff_mem_nhdsSet

IsLocallyClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallyCompactSpace 📖	mathematical	IsLocallyClosed	LocallyCompactSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	Topology.IsInducing.locallyCompactSpace Topology.IsEmbedding.toIsInducing Topology.IsEmbedding.subtypeVal Subtype.range_val

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallyCompactSpace 📖	mathematical	IsOpen	LocallyCompactSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	IsLocallyClosed.locallyCompactSpace isLocallyClosed

IsOpenQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallyCompactSpace 📖	mathematical	IsOpenQuotientMap	LocallyCompactSpace	—	Function.Surjective.forall surjective local_compact_nhds Continuous.continuousAt continuous IsOpenMap.image_mem_nhds isOpenMap Set.image_subset_iff IsCompact.image
weaklyLocallyCompactSpace 📖	mathematical	IsOpenQuotientMap	WeaklyLocallyCompactSpace	—	Function.Surjective.forall surjective WeaklyLocallyCompactSpace.exists_compact_mem_nhds IsCompact.image continuous IsOpenMap.image_mem_nhds isOpenMap

LocallyCompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_hasBasis 📖	mathematical	Filter.HasBasis nhds IsCompact	LocallyCompactSpace	—	Filter.HasBasis.mem_iff Filter.HasBasis.mem_of_mem

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallyCompactSpace 📖	mathematical	LocallyCompactSpace CompactSpace	topologicalSpace	—	Filter.mem_pi nhds_pi set_pi_mem_nhds_iff subset_trans Set.instIsTransSubset forall₂_imp Set.univ_pi_ite isCompact_univ_pi CompactSpace.isCompact_univ LocallyCompactSpace.local_compact_nhds
locallyCompactSpace_of_finite 📖	mathematical	LocallyCompactSpace	topologicalSpace	—	Filter.mem_pi nhds_pi set_pi_mem_nhds_iff Set.finite_univ subset_trans Set.instIsTransSubset isCompact_univ_pi LocallyCompactSpace.local_compact_nhds

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallyCompactSpace 📖	mathematical	—	LocallyCompactSpace instTopologicalSpaceProd	—	Filter.HasBasis.prod_nhds' compact_basis_nhds LocallyCompactSpace.of_hasBasis IsCompact.prod

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallyCompactSpace 📖	mathematical	Topology.IsClosedEmbedding	LocallyCompactSpace	—	Topology.IsInducing.locallyCompactSpace isInducing IsClosed.isLocallyClosed isClosed_range
weaklyLocallyCompactSpace 📖	mathematical	Topology.IsClosedEmbedding	WeaklyLocallyCompactSpace	—	WeaklyLocallyCompactSpace.exists_compact_mem_nhds isCompact_preimage Continuous.continuousAt continuous

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallyCompactSpace 📖	mathematical	Topology.IsInducing IsLocallyClosed Set.range	LocallyCompactSpace	—	IsOpen.mem_nhds Eq.subset Set.instReflSubset Set.mem_range_self nhds_eq_comap comap_nhdsWithin_range nhdsWithin_inter_of_mem nhdsWithin_le_nhds Filter.HasBasis.comap nhdsWithin_hasBasis Filter.HasBasis.restrict_subset compact_basis_nhds LocallyCompactSpace.of_hasBasis isCompact_preimage_iff Set.inter_subset_inter subset_refl IsCompact.inter_right

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallyCompactSpace 📖	mathematical	Topology.IsOpenEmbedding	LocallyCompactSpace	—	Topology.IsInducing.locallyCompactSpace isInducing IsOpen.isLocallyClosed isOpen_range

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compact_basis_nhds 📖	mathematical	—	Filter.HasBasis Set nhds Filter Filter.instMembership IsCompact	—	Filter.hasBasis_self LocallyCompactSpace.local_compact_nhds
disjoint_nhds_cocompact 📖	mathematical	—	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhds Filter.cocompact	—	WeaklyLocallyCompactSpace.exists_compact_mem_nhds Filter.disjoint_of_disjoint_of_mem disjoint_compl_right IsCompact.compl_mem_cocompact
exists_compact_between 📖	mathematical	IsCompact IsOpen Set Set.instHasSubset	interior	—	exists_mem_nhdsSet_isCompact_mapsTo instLocallyCompactPairOfLocallyCompactSpace continuous_id subset_interior_iff_mem_nhdsSet
exists_compact_subset 📖	mathematical	IsOpen Set Set.instMembership	IsCompact interior Set.instHasSubset	—	LocallyCompactSpace.local_compact_nhds IsOpen.mem_nhds mem_interior_iff_mem_nhds
exists_compact_superset 📖	mathematical	IsCompact	Set Set.instHasSubset interior	—	IsCompact.elim_nhds_subcover interior_mem_nhds Finset.isCompact_biUnion HasSubset.Subset.trans Set.instIsTransSubset Set.iUnion₂_subset interior_mono Set.subset_iUnion₂ WeaklyLocallyCompactSpace.exists_compact_mem_nhds
exists_mem_nhdsSet_isCompact_mapsTo 📖	mathematical	Continuous IsCompact IsOpen Set.MapsTo	Set Filter Filter.instMembership nhdsSet	—	IsCompact.elim_nhds_subcover_nhdsSet Finset.isCompact_biUnion Set.mapsTo_iUnion₂ LocallyCompactPair.exists_mem_nhds_isCompact_mapsTo IsOpen.mem_nhds Function.sometimes_spec
instLocallyCompactPairOfLocallyCompactSpace 📖	mathematical	—	LocallyCompactPair	—	local_compact_nhds Continuous.continuousAt
instWeaklyLocallyCompactSpaceForallOfFinite 📖	mathematical	WeaklyLocallyCompactSpace	Pi.topologicalSpace	—	isCompact_univ_pi set_pi_mem_nhds Set.toFinite Subtype.finite WeaklyLocallyCompactSpace.exists_compact_mem_nhds
instWeaklyLocallyCompactSpaceOfCompactSpace 📖	mathematical	—	WeaklyLocallyCompactSpace	—	isCompact_univ Filter.univ_mem
instWeaklyLocallyCompactSpaceOfLocallyCompactSpace 📖	mathematical	—	WeaklyLocallyCompactSpace	—	local_compact_nhds Filter.univ_mem
instWeaklyLocallyCompactSpaceProd 📖	mathematical	—	WeaklyLocallyCompactSpace instTopologicalSpaceProd	—	WeaklyLocallyCompactSpace.exists_compact_mem_nhds IsCompact.prod prod_mem_nhds
local_compact_nhds 📖	mathematical	Set Filter Filter.instMembership nhds	Set.instHasSubset IsCompact	—	LocallyCompactSpace.local_compact_nhds

---

← Back to Index