Commit 2023-09-03 19:50 8c47c403

View on Github →

feat: define weakly locally compact spaces (#6770)

Estimated changes

Modified Mathlib/MeasureTheory/Function/ContinuousMapDense.lean

modified theorem MeasureTheory.Integrable.exists_hasCompactSupport_integral_sub_le

modified theorem MeasureTheory.Integrable.exists_hasCompactSupport_lintegral_sub_le

modified theorem MeasureTheory.Memℒp.exists_hasCompactSupport_integral_rpow_sub_le

modified theorem MeasureTheory.Memℒp.exists_hasCompactSupport_snorm_sub_le

Modified Mathlib/MeasureTheory/Group/Measure.lean

modified theorem MeasureTheory.measure_univ_of_isMulLeftInvariant

Modified Mathlib/MeasureTheory/Measure/Content.lean

modified theorem MeasureTheory.Content.outerMeasure_lt_top_of_isCompact

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean

modified theorem exists_isCompact_isClosed_nhds_one

Modified Mathlib/Topology/Algebra/Group/Compact.lean

added theorem TopologicalSpace.PositiveCompacts.weaklyLocallyCompactSpace_of_group

Modified Mathlib/Topology/CompactOpen.lean

modified theorem ContinuousMap.exists_tendsto_compactOpen_iff_forall

Modified Mathlib/Topology/DiscreteSubset.lean

modified theorem Continuous.discrete_of_tendsto_cofinite_cocompact

modified theorem IsClosed.tendsto_coe_cofinite_iff

Modified Mathlib/Topology/MetricSpace/Baire.lean

Modified Mathlib/Topology/Paracompact.lean

modified theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis

modified theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set

Modified Mathlib/Topology/ProperMap.lean

modified theorem isProperMap_iff_isCompact_preimage

modified theorem isProperMap_iff_tendsto_cocompact

Modified Mathlib/Topology/Separation.lean

modified theorem exists_open_superset_and_isCompact_closure

modified theorem exists_open_with_compact_closure

added theorem locally_compact_of_compact

deleted theorem locally_compact_of_compact_nhds

Modified Mathlib/Topology/Sets/Compacts.lean

Modified Mathlib/Topology/SubsetProperties.lean

deleted theorem exists_compact_mem_nhds

modified theorem exists_compact_superset

Modified Mathlib/Topology/UniformSpace/Compact.lean

modified theorem Continuous.tendstoUniformly

Modified Mathlib/Topology/UniformSpace/CompactConvergence.lean

modified theorem ContinuousMap.tendstoLocallyUniformly_of_tendsto

modified theorem ContinuousMap.tendsto_iff_tendstoLocallyUniformly