Commit 2023-02-01 12:36 da33096a

View on Github →

feat: port Topology.SubsetProperties (#1913)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Maps.lean

added theorem Inducing.mapClusterPt_iff

Created Mathlib/Topology/SubsetProperties.lean

added theorem Bornology.inCompact.isBounded_iff

added def Bornology.inCompact

added theorem ClosedEmbedding.isCompact_preimage

added theorem ClosedEmbedding.tendsto_cocompact

added theorem CompactExhaustion.exists_mem

added theorem CompactExhaustion.find_shiftr

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.unionᵢ_eq

added structure CompactExhaustion

added theorem CompactSpace.elim_nhds_subcover

added theorem ContinuousOn.preimage_clopen_of_clopen

added theorem Embedding.isCompact_iff_isCompact_image

added theorem Filter.Tendsto.isCompact_insert_range

added theorem Filter.Tendsto.isCompact_insert_range_of_cocompact

added theorem Filter.Tendsto.isCompact_insert_range_of_cofinite

added def Filter.coclosedCompact

added def Filter.cocompact

added theorem Filter.cocompact_eq_bot

added theorem Filter.cocompact_eq_cofinite

added theorem Filter.cocompact_le_coclosedCompact

added theorem Filter.cocompact_le_cofinite

added theorem Filter.cocompact_neBot_iff

added theorem Filter.comap_cocompact_le

added theorem Filter.coprod_cocompact

added theorem Filter.coprodᵢ_cocompact

added theorem Filter.hasBasis_coclosedCompact

added theorem Filter.hasBasis_cocompact

added theorem Filter.mem_coclosedCompact

added theorem Filter.mem_coclosed_compact'

added theorem Filter.mem_cocompact'

added theorem Filter.mem_cocompact

added theorem Finset.isCompact_bunionᵢ

added theorem Inducing.isCompact_iff

added theorem IrreducibleSpace.isIrreducible_univ

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 IsClosed.exists_minimal_nonempty_closed_subset

added theorem IsClosed.isCompact

added theorem IsCompact.adherence_nhdset

added theorem IsCompact.compl_mem_coclosedCompact_of_isClosed

added theorem IsCompact.compl_mem_cocompact

added theorem IsCompact.compl_mem_sets

added theorem IsCompact.compl_mem_sets_of_nhdsWithin

added theorem IsCompact.diff

added theorem IsCompact.disjoint_nhdsSet_left

added theorem IsCompact.disjoint_nhdsSet_right

added theorem IsCompact.elim_directed_cover

added theorem IsCompact.elim_finite_subcover

added theorem IsCompact.elim_finite_subcover_image

added theorem IsCompact.elim_finite_subfamily_closed

added theorem IsCompact.elim_nhds_subcover'

added theorem IsCompact.elim_nhds_subcover

added theorem IsCompact.eventually_forall_of_forall_eventually

added theorem IsCompact.finite

added theorem IsCompact.finite_of_discrete

added theorem IsCompact.image

added theorem IsCompact.image_of_continuousOn

added theorem IsCompact.induction_on

added theorem IsCompact.insert

added theorem IsCompact.inter_interᵢ_nonempty

added theorem IsCompact.inter_left

added theorem IsCompact.inter_right

added theorem IsCompact.ne_univ

added theorem IsCompact.nonempty_interᵢ_of_directed_nonempty_compact_closed

added theorem IsCompact.nonempty_interᵢ_of_sequence_nonempty_compact_closed

added theorem IsCompact.prod

added theorem IsCompact.union

added def IsCompact

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 LocallyFinite.finite_nonempty_inter_compact

added theorem LocallyFinite.finite_nonempty_of_compact

added theorem LocallyFinite.finite_of_compact

added theorem Nat.cocompact_eq

added theorem NhdsContainBoxes.comm

added theorem NhdsContainBoxes.symm

added def NhdsContainBoxes

added theorem Prod.noncompactSpace_iff

added theorem Set.Finite.isCompact

added theorem Set.Finite.isCompact_bunionᵢ

added theorem Set.Finite.isCompact_unionₛ

added theorem Set.Subsingleton.isCompact

added theorem Set.Subsingleton.isPreirreducible

added theorem SigmaCompactSpace.of_countable

added theorem Subtype.irreducibleSpace

added theorem Subtype.preirreducibleSpace

added theorem clopen_range_sigmaMk

added theorem cluster_point_of_compact

added def compactCovering

added theorem compactCovering_subset

added theorem compactSpace_of_finite_subfamily_closed

added theorem compact_basis_nhds

added theorem continuousOn_boolIndicator_iff_clopen

added theorem continuous_boolIndicator_iff_clopen

added theorem countable_cover_nhdsWithin_of_sigma_compact

added theorem countable_cover_nhds_of_sigma_compact

added theorem eq_irreducibleComponent

added theorem exists_compact_between

added theorem exists_compact_mem_nhds

added theorem exists_compact_subset

added theorem exists_compact_superset

added theorem exists_mem_compactCovering

added theorem exists_nhds_ne_inf_principal_neBot

added theorem exists_nhds_ne_neBot

added theorem exists_preirreducible

added theorem exists_subset_nhds_of_compactSpace

added theorem exists_subset_nhds_of_isCompact'

added theorem finite_cover_nhds

added theorem finite_cover_nhds_interior

added theorem finite_of_compact_of_discrete

added theorem generalized_tube_lemma

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 isClopen_binterᵢ

added theorem isClopen_binterᵢ_finset

added theorem isClopen_bunionᵢ

added theorem isClopen_bunionᵢ_finset

added theorem isClopen_compl_iff

added theorem isClopen_discrete

added theorem isClopen_empty

added theorem isClopen_iff_frontier_eq_empty

added theorem isClopen_inter_of_disjoint_cover_clopen

added theorem isClopen_interᵢ

added theorem isClopen_unionᵢ

added theorem isClopen_univ

added theorem isClosedMap_snd_of_compactSpace

added theorem isClosed_irreducibleComponent

added theorem isClosed_of_mem_irreducibleComponents

added theorem isCompact_accumulate

added theorem isCompact_compactCovering

added theorem isCompact_diagonal

added theorem isCompact_empty

added theorem isCompact_iff_compactSpace

added theorem isCompact_iff_finite

added theorem isCompact_iff_finite_subcover

added theorem isCompact_iff_finite_subfamily_closed

added theorem isCompact_iff_isCompact_in_subtype

added theorem isCompact_iff_isCompact_univ

added theorem isCompact_iff_ultrafilter_le_nhds

added theorem isCompact_of_finite_subcover

added theorem isCompact_of_finite_subfamily_closed

added theorem isCompact_of_isClosed_subset

added theorem isCompact_open_iff_eq_finite_unionᵢ_of_isTopologicalBasis

added theorem isCompact_pi_infinite

added theorem isCompact_range

added theorem isCompact_singleton

added theorem isCompact_unionᵢ

added theorem isCompact_univ

added theorem isCompact_univ_iff

added theorem isCompact_univ_pi

added theorem isIrreducible_iff_closure

added theorem isIrreducible_iff_interₛ

added theorem isIrreducible_iff_unionₛ_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 local_compact_nhds

added theorem locallyCompactSpace_of_hasBasis

added theorem mem_irreducibleComponent

added theorem nhdsContainBoxes_of_compact

added theorem nhdsContainBoxes_of_singleton

added theorem noncompactSpace_of_neBot

added theorem noncompact_univ

added theorem nonempty_preirreducible_inter

added theorem not_compactSpace_iff

added theorem subset_closure_inter_of_isPreirreducible_of_isOpen

added theorem unionᵢ_compactCovering