Commit 2023-10-11 21:40 13444d80

View on Github →

chore(Topology/SubsetProperties): Refactor SubsetProperties.lean (#7628) Split up the 2000-line Topology/SubsetProperties.lean into several smaller files. Not only is it too huge, but the name is very unhelpful, since actually about 90% of the file is about compactness; I've moved this material into various files inside a new subdirectory Topology/Compactness/.

Estimated changes

Modified Counterexamples/SorgenfreyLine.lean

Modified Mathlib.lean

Modified Mathlib/Geometry/Manifold/Metrizable.lean

Modified Mathlib/Topology/AlexandrovDiscrete.lean

Modified Mathlib/Topology/Category/Profinite/Basic.lean

Created Mathlib/Topology/Clopen.lean

added theorem ContinuousOn.preimage_clopen_of_clopen

added theorem IsClopen.compl

added theorem IsClopen.diff

added theorem IsClopen.inter

added theorem IsClopen.preimage

added theorem IsClopen.prod

added theorem IsClopen.union

added def IsClopen

added theorem Set.Finite.isClopen_biInter

added theorem Set.Finite.isClopen_biUnion

added theorem continuousOn_boolIndicator_iff_clopen

added theorem continuous_boolIndicator_iff_clopen

added theorem isClopen_biInter_finset

added theorem isClopen_biUnion_finset

added theorem isClopen_compl_iff

added theorem isClopen_discrete

added theorem isClopen_empty

added theorem isClopen_iInter_of_finite

added theorem isClopen_iUnion_of_finite

added theorem isClopen_iff_frontier_eq_empty

added theorem isClopen_inter_of_disjoint_cover_clopen

added theorem isClopen_range_inl

added theorem isClopen_range_inr

added theorem isClopen_range_sigmaMk

added theorem isClopen_univ

Modified Mathlib/Topology/CompactOpen.lean

Renamed Mathlib/Topology/SubsetProperties.lean to Mathlib/Topology/Compactness/Compact.lean

deleted theorem CompactExhaustion.exists_mem

deleted theorem CompactExhaustion.find_shiftr

deleted theorem CompactExhaustion.iUnion_eq

deleted theorem CompactExhaustion.mem_diff_shiftr_find

deleted theorem CompactExhaustion.mem_find

deleted theorem CompactExhaustion.mem_iff_find_le

deleted def CompactExhaustion.shiftr

deleted theorem CompactExhaustion.subset_interior

deleted theorem CompactExhaustion.subset_interior_succ

deleted theorem CompactExhaustion.subset_succ

deleted theorem CompactExhaustion.toFun_eq_coe

deleted structure CompactExhaustion

deleted theorem ContinuousOn.preimage_clopen_of_clopen

deleted def Filter.codiscrete

deleted theorem IrreducibleSpace.isIrreducible_univ

deleted theorem IsClopen.compl

deleted theorem IsClopen.diff

deleted theorem IsClopen.inter

deleted theorem IsClopen.preimage

deleted theorem IsClopen.prod

deleted theorem IsClopen.union

deleted def IsClopen

deleted theorem IsClosed.sigmaCompactSpace

deleted theorem IsIrreducible.image

deleted theorem IsIrreducible.isPreirreducible

deleted theorem IsIrreducible.nonempty

deleted def IsIrreducible

deleted theorem IsPreirreducible.image

deleted theorem IsPreirreducible.interior

deleted theorem IsPreirreducible.open_subset

deleted theorem IsPreirreducible.preimage

deleted theorem IsPreirreducible.subset_irreducible

deleted def IsPreirreducible

deleted theorem Set.Finite.isClopen_biInter

deleted theorem Set.Finite.isClopen_biUnion

deleted theorem Set.Subsingleton.isPreirreducible

deleted theorem SigmaCompactSpace.of_countable

deleted theorem Subtype.irreducibleSpace

deleted theorem Subtype.preirreducibleSpace

deleted def compactCovering

deleted theorem compactCovering_subset

deleted theorem compact_basis_nhds

deleted theorem continuousOn_boolIndicator_iff_clopen

deleted theorem continuous_boolIndicator_iff_clopen

deleted theorem countable_cover_nhdsWithin_of_sigma_compact

deleted theorem countable_cover_nhds_of_sigma_compact

deleted theorem disjoint_nhds_cocompact

deleted theorem eq_irreducibleComponent

deleted theorem exists_compact_between

deleted theorem exists_compact_subset

deleted theorem exists_compact_superset

deleted theorem exists_mem_compactCovering

deleted theorem exists_preirreducible

deleted theorem iUnion_compactCovering

deleted def irreducibleComponent

deleted theorem irreducibleComponent_mem_irreducibleComponents

deleted theorem irreducibleComponent_property

deleted def irreducibleComponents

deleted theorem irreducibleComponents_eq_maximals_closed

deleted theorem irreducibleSpace_def

deleted theorem isClopen_biInter_finset

deleted theorem isClopen_biUnion_finset

deleted theorem isClopen_compl_iff

deleted theorem isClopen_discrete

deleted theorem isClopen_empty

deleted theorem isClopen_iInter_of_finite

deleted theorem isClopen_iUnion_of_finite

deleted theorem isClopen_iff_frontier_eq_empty

deleted theorem isClopen_inter_of_disjoint_cover_clopen

deleted theorem isClopen_range_inl

deleted theorem isClopen_range_inr

deleted theorem isClopen_range_sigmaMk

deleted theorem isClopen_univ

deleted theorem isClosed_and_discrete_iff

deleted theorem isClosed_irreducibleComponent

deleted theorem isClosed_of_mem_irreducibleComponents

deleted theorem isCompact_compactCovering

deleted theorem isIrreducible_iff_closure

deleted theorem isIrreducible_iff_sInter

deleted theorem isIrreducible_iff_sUnion_closed

deleted theorem isIrreducible_irreducibleComponent

deleted theorem isIrreducible_singleton

deleted theorem isPreirreducible_empty

deleted theorem isPreirreducible_iff_closed_union_closed

deleted theorem isPreirreducible_iff_closure

deleted theorem isPreirreducible_singleton

deleted theorem local_compact_nhds

deleted theorem locallyCompactSpace_of_hasBasis

deleted theorem mem_irreducibleComponent

deleted theorem nonempty_preirreducible_inter

deleted theorem subset_closure_inter_of_isPreirreducible_of_isOpen

Created Mathlib/Topology/Compactness/LocallyCompact.lean

added theorem compact_basis_nhds

added theorem disjoint_nhds_cocompact

added theorem exists_compact_between

added theorem exists_compact_subset

added theorem exists_compact_superset

added theorem local_compact_nhds

added theorem locallyCompactSpace_of_hasBasis

Renamed Mathlib/Topology/Paracompact.lean to Mathlib/Topology/Compactness/Paracompact.lean

Created Mathlib/Topology/Compactness/SigmaCompact.lean

added theorem CompactExhaustion.exists_mem

added theorem CompactExhaustion.find_shiftr

added theorem CompactExhaustion.iUnion_eq

added theorem CompactExhaustion.mem_diff_shiftr_find

added theorem CompactExhaustion.mem_find

added theorem CompactExhaustion.mem_iff_find_le

added def CompactExhaustion.shiftr

added theorem CompactExhaustion.subset_interior

added theorem CompactExhaustion.subset_interior_succ

added theorem CompactExhaustion.subset_succ

added theorem CompactExhaustion.toFun_eq_coe

added structure CompactExhaustion

added theorem IsClosed.sigmaCompactSpace

added theorem SigmaCompactSpace.of_countable

added def compactCovering

added theorem compactCovering_subset

added theorem countable_cover_nhdsWithin_of_sigma_compact

added theorem countable_cover_nhds_of_sigma_compact

added theorem exists_mem_compactCovering

added theorem iUnion_compactCovering

added theorem isCompact_compactCovering

Modified Mathlib/Topology/Connected.lean

Modified Mathlib/Topology/DiscreteQuotient.lean

Modified Mathlib/Topology/DiscreteSubset.lean

added def Filter.codiscrete

added theorem isClosed_and_discrete_iff

Modified Mathlib/Topology/EMetricSpace/Paracompact.lean

Created Mathlib/Topology/Irreducible.lean

added theorem IrreducibleSpace.isIrreducible_univ

added theorem IsIrreducible.image

added theorem IsIrreducible.isPreirreducible

added theorem IsIrreducible.nonempty

added def IsIrreducible

added theorem IsPreirreducible.image

added theorem IsPreirreducible.interior

added theorem IsPreirreducible.open_subset

added theorem IsPreirreducible.preimage

added theorem IsPreirreducible.subset_irreducible

added def IsPreirreducible

added theorem Set.Subsingleton.isPreirreducible

added theorem Subtype.irreducibleSpace

added theorem Subtype.preirreducibleSpace

added theorem eq_irreducibleComponent

added theorem exists_preirreducible

added def irreducibleComponent

added theorem irreducibleComponent_mem_irreducibleComponents

added theorem irreducibleComponent_property

added def irreducibleComponents

added theorem irreducibleComponents_eq_maximals_closed

added theorem irreducibleSpace_def

added theorem isClosed_irreducibleComponent

added theorem isClosed_of_mem_irreducibleComponents

added theorem isIrreducible_iff_closure

added theorem isIrreducible_iff_sInter

added theorem isIrreducible_iff_sUnion_closed

added theorem isIrreducible_irreducibleComponent

added theorem isIrreducible_singleton

added theorem isPreirreducible_empty

added theorem isPreirreducible_iff_closed_union_closed

added theorem isPreirreducible_iff_closure

added theorem isPreirreducible_singleton

added theorem mem_irreducibleComponent

added theorem nonempty_preirreducible_inter

added theorem subset_closure_inter_of_isPreirreducible_of_isOpen

Modified Mathlib/Topology/LocallyConstant/Basic.lean

Modified Mathlib/Topology/PartitionOfUnity.lean

Modified Mathlib/Topology/QuasiSeparated.lean

Modified Mathlib/Topology/Separation.lean

Modified Mathlib/Topology/Sequences.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean