DiscreteSubset

📁 Source: Mathlib/Topology/DiscreteSubset.lean

Statistics

Metric	Count
Definitions codiscrete, codiscreteWithin	2
Theorems discrete_of_tendsto_cofinite_cocompact, mono, self_mem_codiscreteWithin, tendsto_coe_cofinite_iff, tendsto_coe_cofinite_of_discreteTopology, tendsto_coe_cofinite_of_isDiscrete, eq_of_specializes, image, image_of_isOpenMap, image_of_isOpenMap_of_isOpen, nhdsWithin, of_nhdsWithin, preimage, preimage', univ, isDiscrete_range, isDiscrete_range, compl_mem_codiscrete, of_accPt, isDiscrete, codiscreteWithin_iff_locallyEmptyComplementWithin, codiscreteWithin_iff_locallyFiniteComplementWithin, codiscrete_le_cofinite, compl_mem_codiscrete_iff, discreteTopology_biUnion_finset, discreteTopology_iUnion_finite, discreteTopology_iUnion_fintype, discreteTopology_of_codiscreteWithin, discreteTopology_of_noAccPts, discreteTopology_subtype_iff, discreteTopology_subtype_iff', discreteTopology_union, isClosed_and_discrete_iff, isClosed_sdiff_of_codiscreteWithin, isDiscrete_iff_forall_exists_isOpen, isDiscrete_iff_nhdsNE, isDiscrete_iff_nhdsWithin, isDiscrete_of_codiscreteWithin, isDiscrete_univ_iff, mem_codiscrete, mem_codiscrete', mem_codiscreteWithin, mem_codiscreteWithin_accPt, mem_codiscreteWithin_iff_forall_mem_nhdsNE, mem_codiscrete_accPt, mem_codiscrete_subtype_iff_mem_codiscreteWithin, nhdsNE_of_nhdsNE_sdiff_finite, tendsto_cofinite_cocompact_iff, tendsto_cofinite_cocompact_of_discrete	49
Total	51

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discrete_of_tendsto_cofinite_cocompact 📖	mathematical	Continuous Filter.Tendsto Filter.cofinite Filter.cocompact	DiscreteTopology	—	discreteTopology_iff_isOpen_singleton WeaklyLocallyCompactSpace.exists_compact_mem_nhds mem_nhds_iff Set.Finite.subset tendsto_cofinite_cocompact_iff Set.preimage_mono isOpen_singleton_of_finite_mem_nhds IsOpen.mem_nhds IsOpen.preimage

Filter

Definitions

Name	Category	Theorems
codiscrete 📖	CompOp	11 math math: MeromorphicOn.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top, compl_mem_codiscrete_iff, mem_codiscrete', mem_codiscrete, mem_codiscrete_accPt, AnalyticOnNhd.preimage_zero_mem_codiscrete, circleMap_preimage_codiscrete, AnalyticOnNhd.codiscrete_setOf_analyticOrderAt_eq_zero_or_top, Set.Finite.compl_mem_codiscrete, mem_codiscrete_subtype_iff_mem_codiscreteWithin, codiscrete_le_cofinite
codiscreteWithin 📖	CompOp	22 math math: mem_codiscreteWithin_iff_forall_mem_nhdsNE, Function.locallyFinsuppWithin.eq_zero_codiscreteWithin, MeromorphicOn.analyticAt_mem_codiscreteWithin, codiscreteWithin_iff_locallyEmptyComplementWithin, MeromorphicOn.meromorphicNFAt_mem_codiscreteWithin, AnalyticOnNhd.codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top, circleMap_preimage_codiscrete, MeromorphicOn.eventually_codiscreteWithin_analyticAt, AnalyticOnNhd.eqOn_or_eventually_ne_of_preconnected, codiscreteWithin_iff_locallyFiniteComplementWithin, mem_codiscreteWithin_accPt, ae_restrict_le_codiscreteWithin, supportDiscreteWithin_iff_locallyFiniteWithin, mem_codiscreteWithin, self_mem_codiscreteWithin, MeromorphicOn.extract_zeros_poles, codiscreteWithin.mono, AnalyticOnNhd.map_codiscreteWithin, AnalyticOnNhd.preimage_zero_mem_codiscreteWithin, mem_codiscrete_subtype_iff_mem_codiscreteWithin, AnalyticOnNhd.eqOn_zero_or_eventually_ne_zero_of_preconnected, toMeromorphicNFOn_eqOn_codiscrete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
self_mem_codiscreteWithin 📖	mathematical	—	Set Filter instMembership codiscreteWithin	—	sdiff_self principal_empty

Filter.codiscreteWithin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	mathematical	Set Set.instHasSubset	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.codiscreteWithin	—	LE.le.trans biSup_mono iSup₂_mono nhdsWithin_mono Set.diff_subset_diff subset_refl Set.instReflSubset

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_coe_cofinite_iff 📖	mathematical	—	Filter.Tendsto Set Set.instMembership Filter.cofinite Filter.cocompact IsDiscrete	—	Continuous.discrete_of_tendsto_cofinite_cocompact Subtype.t1Space continuous_subtype_val tendsto_coe_cofinite_of_isDiscrete
tendsto_coe_cofinite_of_discreteTopology 📖	mathematical	IsDiscrete	Filter.Tendsto Set Set.instMembership Filter.cofinite Filter.cocompact	—	tendsto_coe_cofinite_of_isDiscrete
tendsto_coe_cofinite_of_isDiscrete 📖	mathematical	IsDiscrete	Filter.Tendsto Set Set.instMembership Filter.cofinite Filter.cocompact	—	tendsto_cofinite_cocompact_of_discrete IsDiscrete.to_subtype Topology.IsClosedEmbedding.tendsto_cocompact isClosedEmbedding_subtypeVal

IsDiscrete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_specializes 📖	—	IsDiscrete Specializes Set Set.instMembership	—	—	Topology.IsInducing.specializes_iff Topology.IsInducing.subtypeVal specializes_iff_eq instT1SpaceOfDiscreteTopology to_subtype
image 📖	mathematical	IsDiscrete Topology.IsEmbedding	Set.image	—	of_nhdsWithin Filter.map_pure nhdsWithin Topology.IsEmbedding.map_nhdsWithin_eq le_refl
image_of_isOpenMap 📖	mathematical	IsDiscrete IsOpenMap	Set.image	—	of_nhdsWithin Filter.map_pure nhdsWithin nhdsWithin.eq_1 Filter.map_inf Filter.map_principal le_imp_le_of_le_of_le inf_le_inf IsOpenMap.nhds_le le_refl
image_of_isOpenMap_of_isOpen 📖	mathematical	IsDiscrete IsOpenMap IsOpen	Set.image	—	of_nhdsWithin IsOpen.nhdsWithin_eq Filter.map_pure nhdsWithin IsOpenMap.nhds_le
nhdsWithin 📖	mathematical	IsDiscrete Set Set.instMembership	nhdsWithin Filter Filter.instPure	—	isDiscrete_iff_nhdsWithin
of_nhdsWithin 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhdsWithin Filter.instPure	IsDiscrete	—	isDiscrete_iff_nhdsWithin LE.le.antisymm pure_le_nhdsWithin
preimage 📖	—	IsDiscrete ContinuousOn Set.preimage	—	—	of_nhdsWithin Filter.map_le_map_iff Filter.map_pure nhdsWithin Filter.Tendsto.eq_1 ContinuousWithinAt.tendsto_nhdsWithin ContinuousOn.continuousWithinAt Set.mapsTo_preimage
preimage' 📖	—	IsDiscrete ContinuousOn Set.preimage Set Set.instSingletonSet	—	—	of_nhdsWithin Eq.le nhdsWithin inf_eq_right nhdsWithin_le_nhds le_imp_le_of_le_of_le inf_le_inf le_refl Filter.Tendsto.le_comap ContinuousWithinAt.tendsto_nhdsWithin ContinuousOn.continuousWithinAt Filter.comap_pure nhdsWithin.eq_1
univ 📖	mathematical	—	IsDiscrete Set.univ	—	isDiscrete_univ_iff

IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDiscrete_range 📖	mathematical	Topology.IsEmbedding	IsDiscrete Set.range	—	Set.image_univ IsDiscrete.image IsDiscrete.univ

IsOpenMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDiscrete_range 📖	mathematical	IsOpenMap	IsDiscrete Set.range	—	Set.image_univ IsDiscrete.image_of_isOpenMap_of_isOpen IsDiscrete.univ isOpen_univ

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl_mem_codiscrete 📖	mathematical	—	Set Filter Filter.instMembership Filter.codiscrete Compl.compl Set.instCompl	—	codiscrete_le_cofinite compl_compl

Set.Infinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_accPt 📖	mathematical	—	Set.Infinite	—	Set.Finite.compl_mem_codiscrete compl_compl mem_codiscrete_accPt

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDiscrete 📖	mathematical	Set.Subsingleton	IsDiscrete	—	Set.subsingleton_coe Subsingleton.discreteTopology

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codiscreteWithin_iff_locallyEmptyComplementWithin 📖	mathematical	—	Set Filter Filter.instMembership Filter.codiscreteWithin nhdsWithin Compl.compl Set.instCompl Set.instSingletonSet Set.instInter Set.instSDiff Set.instEmptyCollection	—	Set.compl_inter_self Filter.exists_mem_subset_iff Disjoint.subset_compl_right Set.disjoint_iff_inter_eq_empty
codiscreteWithin_iff_locallyFiniteComplementWithin 📖	mathematical	—	Set Filter Filter.instMembership Filter.codiscreteWithin nhds Set.Finite Set.instInter Set.instSDiff	—	codiscreteWithin_iff_locallyEmptyComplementWithin insert_mem_nhds_iff Set.inter_comm Set.inter_insert_of_mem Set.instLawfulSingleton Set.inter_insert_of_notMem nhdsNE_of_nhdsNE_sdiff_finite mem_nhdsWithin_of_mem_nhds Set.diff_self_inter Set.diff_inter_self
codiscrete_le_cofinite 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.codiscrete Filter.cofinite	—	compl_compl compl_mem_codiscrete_iff Set.Finite.isClosed IsDiscrete.to_subtype Set.Finite.isDiscrete
compl_mem_codiscrete_iff 📖	mathematical	—	Set Filter Filter.instMembership Filter.codiscrete Compl.compl Set.instCompl IsClosed DiscreteTopology Set.Elem instTopologicalSpaceSubtype Set.instMembership	—	mem_codiscrete compl_compl isDiscrete_iff_discreteTopology isClosed_and_discrete_iff
discreteTopology_biUnion_finset 📖	mathematical	DiscreteTopology Set.Elem instTopologicalSpaceSubtype Set Set.instMembership IsClosed	Set.iUnion Finset Finset.instMembership	—	Set.compl_iUnion Filter.biInter_finset_mem compl_mem_codiscrete_iff
discreteTopology_iUnion_finite 📖	mathematical	DiscreteTopology Set.Elem instTopologicalSpaceSubtype Set Set.instMembership IsClosed	Set.iUnion	—	Set.iUnion_congr_Prop Set.iUnion_true discreteTopology_biUnion_finset
discreteTopology_iUnion_fintype 📖	mathematical	DiscreteTopology Set.Elem instTopologicalSpaceSubtype Set Set.instMembership IsClosed	Set.iUnion	—	discreteTopology_iUnion_finite
discreteTopology_of_codiscreteWithin 📖	mathematical	Set Filter Filter.instMembership Filter.codiscreteWithin Compl.compl Set.instCompl	IsDiscrete Set.instInter	—	isDiscrete_of_codiscreteWithin
discreteTopology_of_noAccPts 📖	mathematical	AccPt Filter.principal	DiscreteTopology Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	—
discreteTopology_subtype_iff 📖	mathematical	—	DiscreteTopology Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Filter Filter.instInf nhdsWithin Compl.compl Set.instCompl Set.instSingletonSet Filter.principal Bot.bot Filter.instBot	—	—
discreteTopology_subtype_iff' 📖	mathematical	—	DiscreteTopology Set.Elem instTopologicalSpaceSubtype Set Set.instMembership IsOpen Set.instInter Set.instSingletonSet	—	—
discreteTopology_union 📖	mathematical	—	DiscreteTopology Set.Elem Set Set.instUnion instTopologicalSpaceSubtype Set.instMembership	—	Set.compl_union Filter.inter_mem compl_mem_codiscrete_iff
isClosed_and_discrete_iff 📖	mathematical	—	IsClosed IsDiscrete Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet Filter.principal	—	isDiscrete_iff_nhdsNE isClosed_iff_clusterPt not_imp_not clusterPt_iff_not_disjoint disjoint_iff Disjoint.mono_left nhdsWithin_le_nhds inf_assoc inf_of_le_right
isClosed_sdiff_of_codiscreteWithin 📖	mathematical	Set Filter Filter.instMembership Filter.codiscreteWithin	IsClosed Set.instSDiff	—	isOpen_compl_iff isOpen_iff_eventually Filter.mp_mem eventually_nhdsWithin_iff Filter.disjoint_principal_right mem_codiscreteWithin Filter.univ_mem' Filter.eventually_iff_exists_mem IsClosed.compl_mem_nhds
isDiscrete_iff_forall_exists_isOpen 📖	mathematical	—	IsDiscrete IsOpen Set Set.instInter Set.instSingletonSet	—	isDiscrete_iff_discreteTopology discreteTopology_subtype_iff'
isDiscrete_iff_nhdsNE 📖	mathematical	—	IsDiscrete Filter Filter.instInf nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet Filter.principal Bot.bot Filter.instBot	—	isDiscrete_iff_discreteTopology discreteTopology_subtype_iff
isDiscrete_iff_nhdsWithin 📖	mathematical	—	IsDiscrete nhdsWithin Filter Filter.instPure	—	nhds_induced Filter.map_injective Subtype.val_injective Filter.map_comap Subtype.range_coe_subtype
isDiscrete_of_codiscreteWithin 📖	mathematical	Set Filter Filter.instMembership Filter.codiscreteWithin Compl.compl Set.instCompl	IsDiscrete Set.instInter	—	Set.compl_union compl_compl isDiscrete_iff_nhdsNE sdiff_compl
isDiscrete_univ_iff 📖	mathematical	—	IsDiscrete Set.univ DiscreteTopology	—	nhdsWithin_univ
mem_codiscrete 📖	mathematical	—	Set Filter Filter.instMembership Filter.codiscrete Disjoint Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhdsWithin Compl.compl Set.instCompl Set.instSingletonSet Filter.principal	—	Set.compl_eq_univ_diff sdiff_sdiff_right_self inf_of_le_right
mem_codiscrete' 📖	mathematical	—	Set Filter Filter.instMembership Filter.codiscrete IsOpen IsDiscrete Compl.compl Set.instCompl	—	mem_codiscrete isClosed_compl_iff isClosed_and_discrete_iff
mem_codiscreteWithin 📖	mathematical	—	Set Filter Filter.instMembership Filter.codiscreteWithin Disjoint Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhdsWithin Compl.compl Set.instCompl Set.instSingletonSet Filter.principal Set.instSDiff	—	—
mem_codiscreteWithin_accPt 📖	mathematical	—	Set Filter Filter.instMembership Filter.codiscreteWithin AccPt Filter.principal Set.instSDiff	—	—
mem_codiscreteWithin_iff_forall_mem_nhdsNE 📖	mathematical	—	Set Filter Filter.instMembership Filter.codiscreteWithin nhdsWithin Compl.compl Set.instCompl Set.instSingletonSet Set.instUnion	—	Set.compl_diff
mem_codiscrete_accPt 📖	mathematical	—	Set Filter Filter.instMembership Filter.codiscrete AccPt Filter.principal Compl.compl Set.instCompl	—	—
mem_codiscrete_subtype_iff_mem_codiscreteWithin 📖	mathematical	—	Set Set.Elem Filter Filter.instMembership Filter.codiscrete instTopologicalSpaceSubtype Set.instMembership Filter.codiscreteWithin Set.image	—	compl_compl nhdsWithin_subtype Filter.mem_comap mem_nhdsWithin Set.image_val_compl Set.image_singleton tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within Continuous.continuousWithinAt continuous_subtype_val Filter.Eventually.mono eventually_mem_nhdsWithin Set.ext Subtype.coe_preimage_self Set.preimage_image_eq Filter.tendsto_def
nhdsNE_of_nhdsNE_sdiff_finite 📖	mathematical	Set Filter Filter.instMembership nhdsWithin Compl.compl Set.instCompl Set.instSingletonSet	Set.instSDiff	—	mem_nhdsWithin isClosed_compl_iff Set.compl_diff IsClosed.union Set.Finite.isClosed Set.Finite.diff Set.toFinite
tendsto_cofinite_cocompact_iff 📖	mathematical	—	Filter.Tendsto Filter.cofinite Filter.cocompact Set.Finite Set.preimage	—	Filter.HasBasis.tendsto_right_iff Filter.hasBasis_cocompact
tendsto_cofinite_cocompact_of_discrete 📖	mathematical	Filter.Tendsto Filter.cocompact	Filter.cofinite	—	Filter.cocompact_eq_cofinite

---

← Back to Index