Lindelof

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

Statistics

Metric	Count
Definitions coLindelof, coclosedLindelof, HereditarilyLindelofSpace, IsHereditarilyLindelof, IsLindelof, LindelofSpace, NonLindelofSpace	7
Theorems LindelofSpace, coLindelof_eq_bot, coLindelof_neBot_iff, comap_coLindelof_le, isLindelof_biUnion, to_Lindelof, isHereditarilyLindelof_univ, isLindelof, of_forall_isOpen, HereditarilyLindelof_LindelofSets, isLindelof, isLindelof, isLindelof, isLindelof_subset, adherence_nhdset, compl_mem_coLindelof, compl_mem_sets, compl_mem_sets_of_nhdsWithin, countable, countable_of_discrete, countable_of_isDiscrete, diff, disjoint_nhdsSet_left, disjoint_nhdsSet_right, elim_countable_subcover, elim_countable_subcover_image, elim_countable_subfamily_closed, elim_nhds_subcover, elim_nhds_subcover', image, image_of_continuousOn, indexed_countable_subcover, induction_on, insert, inter_iInter_nonempty, inter_left, inter_right, ne_univ, of_coe, of_isClosed_subset, union, compl_mem_coclosedLindelof_of_isClosed, isLindelof, elim_nhds_subcover, isLindelof_univ, of_continuous_surjective, nonLindelof_univ, LindelofSpace, lindelofSpace, LindelofSpace, lindelofSpace, toHereditarilyLindelof, isLindelof, isLindelof_biUnion, isLindelof_sUnion, isLindelof, isLindelof_biUnion, isLindelof_sUnion, isLindelof, lindelofSpace, isLindelof_iff, isLindelof_insert_range_of_coLindelof, LindelofSpace, isLindelof_preimage, nonLindelofSpace, tendsto_coLindelof, isLindelof_iff, isLindelof_iff, isLindelof_preimage, cluster_point_of_Lindelof, coLindelof_le_coclosedLindelof, coLindelof_le_cofinite, countable_cover_nhds, countable_cover_nhds_interior, countable_of_Lindelof_of_discrete, eq_closed_inter_countable, eq_closed_inter_nat, eq_open_union_countable, eq_open_union_nat, hasBasis_coLindelof, hasBasis_coclosedLindelof, instHereditarilyLindelofSpaceSubtype, instLindelofSpaceOfCompactSpace, instLindelofSpaceOfSigmaCompactSpace, instLindelofSpaceSigmaOfCountable, instLindelofSpaceSum, instNeBotCoLindelofOfNonLindelofSpace, instNeBotCoclosedLindelofOfNonLindelofSpace, isLindelof_accumulate, isLindelof_diagonal, isLindelof_empty, isLindelof_iUnion, isLindelof_iff_LindelofSpace, isLindelof_iff_countable, isLindelof_iff_countable_subcover, isLindelof_iff_countable_subfamily_closed, isLindelof_iff_isLindelof_univ, isLindelof_iff_lindelofSpace, isLindelof_of_countable_subcover, isLindelof_of_countable_subfamily_closed, isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis, isLindelof_range, isLindelof_singleton, isLindelof_univ, isLindelof_univ_iff, lindelofSpace_of_countable_subfamily_closed, mem_coLindelof, mem_coLindelof', mem_coclosedLindelof, mem_coclosed_Lindelof', nonLindelofSpace_of_neBot, nonLindelof_univ, not_LindelofSpace_iff	113
Total	120

Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
LindelofSpace 📖	mathematical	—	LindelofSpace	—	Set.Countable.isLindelof Set.countable_univ

Filter

Definitions

Name	Category	Theorems
coLindelof 📖	CompOp	11 math math: mem_coLindelof', coLindelof_neBot_iff, IsLindelof.compl_mem_coLindelof, hasBasis_coLindelof, coLindelof_le_cofinite, coLindelof_eq_bot, comap_coLindelof_le, mem_coLindelof, coLindelof_le_coclosedLindelof, instNeBotCoLindelofOfNonLindelofSpace, Topology.IsClosedEmbedding.tendsto_coLindelof
coclosedLindelof 📖	CompOp	6 math math: instNeBotCoclosedLindelofOfNonLindelofSpace, hasBasis_coclosedLindelof, mem_coclosedLindelof, coLindelof_le_coclosedLindelof, IsLindeof.compl_mem_coclosedLindelof_of_isClosed, mem_coclosed_Lindelof'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coLindelof_eq_bot 📖	mathematical	—	coLindelof Bot.bot Filter instBot	—	HasBasis.eq_bot_iff hasBasis_coLindelof isLindelof_univ Set.compl_univ
coLindelof_neBot_iff 📖	mathematical	—	NeBot coLindelof NonLindelofSpace	—	nonLindelofSpace_of_neBot instNeBotCoLindelofOfNonLindelofSpace
comap_coLindelof_le 📖	mathematical	Continuous	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder comap coLindelof	—	HasBasis.le_basis_iff HasBasis.comap hasBasis_coLindelof IsLindelof.image Set.subset_preimage_image

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLindelof_biUnion 📖	mathematical	IsLindelof	Set.iUnion Finset instMembership	—	Set.Finite.isLindelof_biUnion finite_toSet

HereditarilyLindelof

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_Lindelof 📖	mathematical	—	LindelofSpace	—	IsHereditarilyLindelof.isLindelof HereditarilyLindelofSpace.isHereditarilyLindelof_univ

HereditarilyLindelofSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isHereditarilyLindelof_univ 📖	mathematical	—	IsHereditarilyLindelof Set.univ	—	—
isLindelof 📖	mathematical	—	IsLindelof	—	isHereditarilyLindelof_univ Set.subset_univ
of_forall_isOpen 📖	mathematical	IsLindelof	HereditarilyLindelofSpace	—	isLindelof_of_countable_subcover IsLindelof.elim_countable_subcover isOpen_iUnion subset_rfl Set.instReflSubset HasSubset.Subset.trans Set.instIsTransSubset

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLindelof 📖	mathematical	—	IsLindelof	—	IsLindelof.of_isClosed_subset isLindelof_univ Set.subset_univ

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLindelof 📖	mathematical	IsCompact	IsLindelof	—	—

IsHereditarilyLindelof

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLindelof 📖	mathematical	IsHereditarilyLindelof	IsLindelof	—	isLindelof_subset Set.Subset.rfl
isLindelof_subset 📖	mathematical	IsHereditarilyLindelof Set Set.instHasSubset	IsLindelof	—	—

IsLindelof

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adherence_nhdset 📖	mathematical	IsLindelof Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.principal IsOpen Set Set.instMembership	Filter.instMembership	—	Filter.eq_or_neBot Filter.mem_of_eq_bot countableInterFilter_inf countableInterFilter_principal inf_le_of_left_le ClusterPt.of_inf_left inter_mem_nhdsWithin IsOpen.mem_nhds Filter.empty_mem_iff_bot Set.compl_inter_self Filter.NeBot.ne ClusterPt.of_inf_right
compl_mem_coLindelof 📖	mathematical	IsLindelof	Set Filter Filter.instMembership Filter.coLindelof Compl.compl Set.instCompl	—	Filter.HasBasis.mem_of_mem hasBasis_coLindelof
compl_mem_sets 📖	—	IsLindelof Set Filter Filter.instMembership Filter.instInf nhds Compl.compl Set.instCompl	—	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq compl_compl inf_assoc countableInterFilter_inf countableInterFilter_principal inf_le_right
compl_mem_sets_of_nhdsWithin 📖	—	IsLindelof Set Filter Filter.instMembership nhdsWithin Compl.compl Set.instCompl	—	—	compl_mem_sets Filter.disjoint_principal_right disjoint_right_comm Filter.HasBasis.disjoint_iff_left Filter.basis_sets
countable 📖	mathematical	IsLindelof	Set.Countable	—	Set.countable_coe_iff countable_of_Lindelof_of_discrete isLindelof_iff_lindelofSpace
countable_of_discrete 📖	mathematical	IsLindelof	Set.Countable	—	nhds_discrete elim_nhds_subcover Set.Countable.mono Set.biUnion_of_singleton
countable_of_isDiscrete 📖	mathematical	IsLindelof IsDiscrete	Set.Countable	—	countable IsDiscrete.to_subtype
diff 📖	mathematical	IsLindelof IsOpen	Set Set.instSDiff	—	inter_right isClosed_compl_iff
disjoint_nhdsSet_left 📖	mathematical	IsLindelof	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhdsSet nhds	—	Disjoint.mono_left nhds_le_nhdsSet elim_nhds_subcover IsOpen.mem_nhds Filter.HasBasis.disjoint_iff_left hasBasis_nhdsSet isOpen_biUnion Set.compl_iUnion₂ countable_bInter_mem nhds_basis_opens Function.sometimes_spec
disjoint_nhdsSet_right 📖	mathematical	IsLindelof	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhdsSet nhds	—	disjoint_nhdsSet_left
elim_countable_subcover 📖	mathematical	IsLindelof IsOpen Set Set.instHasSubset Set.iUnion	Set.Countable Set.instMembership	—	Set.Subset.trans Set.Countable.biUnion_iff Set.sUnion_subset Set.iUnion_congr_Prop Set.iUnion_exists Set.biUnion_and' Set.mem_biUnion Function.sometimes_spec Set.mem_iUnion mem_nhdsWithin_of_mem_nhds IsOpen.mem_nhds Set.iUnion_iUnion_eq_left Set.Subset.refl induction_on
elim_countable_subcover_image 📖	mathematical	IsLindelof IsOpen Set Set.instHasSubset Set.iUnion Set.instMembership	Set.Countable	—	elim_countable_subcover Set.biUnion_eq_iUnion Subtype.coe_preimage_self Set.Countable.image Set.biUnion_image
elim_countable_subfamily_closed 📖	mathematical	IsLindelof IsClosed Set Set.instInter Set.iInter Set.instEmptyCollection	Set.Countable Set.instMembership	—	Set.compl_iInter Set.disjoint_compl_left_iff_subset Set.compl_iUnion compl_compl Disjoint.symm Set.disjoint_iff_inter_eq_empty elim_countable_subcover Set.iUnion_congr_Prop Set.iInter_congr_Prop
elim_nhds_subcover 📖	mathematical	IsLindelof Set Filter Filter.instMembership nhds	Set.Countable Set.instMembership Set.instHasSubset Set.iUnion	—	elim_nhds_subcover' Set.Countable.image Set.biUnion_image
elim_nhds_subcover' 📖	mathematical	IsLindelof Set Filter Filter.instMembership nhds	Set.Countable Set.Elem Set.instHasSubset Set.iUnion Set.instMembership	—	elim_countable_subcover isOpen_interior Set.mem_iUnion mem_interior_iff_mem_nhds Set.Subset.trans Set.iUnion₂_subset interior_subset Set.subset_iUnion_of_subset Set.Subset.refl
image 📖	mathematical	IsLindelof Continuous	Set.image	—	image_of_continuousOn Continuous.continuousOn
image_of_continuousOn 📖	mathematical	IsLindelof ContinuousOn	Set.image	—	Filter.comap_inf_principal_neBot_of_image_mem Filter.le_principal_iff countableInterFilter_inf instCountableInterFilterComap countableInterFilter_principal inf_le_right Set.mem_image_of_mem nhdsWithin.eq_1 instAssociativeMin_mathlib instCommutativeMin_mathlib instIdempotentOpMin_mathlib Filter.Tendsto.inf Filter.tendsto_comap Filter.Tendsto.neBot ClusterPt.neBot
indexed_countable_subcover 📖	—	IsLindelof IsOpen Set Set.instHasSubset Set.iUnion	—	—	elim_countable_subcover Set.eq_empty_or_nonempty Set.subset_eq_empty Set.iUnion_congr_Prop Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty Set.countable_iff_exists_surjective HasSubset.Subset.trans Set.instIsTransSubset Set.iUnion₂_subset_iff Set.subset_iUnion_of_subset subset_of_eq Set.instReflSubset
induction_on 📖	—	IsLindelof Set.sUnion Set Filter Filter.instMembership nhdsWithin	—	—	compl_mem_sets_of_nhdsWithin Filter.countableInter_ofCountableUnion compl_compl
insert 📖	mathematical	IsLindelof	Set Set.instInsert	—	union isLindelof_singleton
inter_iInter_nonempty 📖	—	IsLindelof IsClosed Set.Countable Set.Nonempty Set Set.instInter Set.iInter Set.instMembership	—	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq Mathlib.Tactic.Push.not_and_eq elim_countable_subfamily_closed
inter_left 📖	mathematical	IsLindelof	Set Set.instInter	—	inter_right Set.inter_comm
inter_right 📖	mathematical	IsLindelof	Set Set.instInter	—	le_inf_iff Filter.inf_principal IsClosed.mem_of_nhdsWithin_neBot ClusterPt.mono
ne_univ 📖	—	IsLindelof	—	—	nonLindelof_univ
of_coe 📖	mathematical	—	IsLindelof	—	isLindelof_iff_lindelofSpace
of_isClosed_subset 📖	—	IsLindelof Set Set.instHasSubset	—	—	inter_right Set.inter_eq_self_of_subset_right
union 📖	mathematical	IsLindelof	Set Set.instUnion	—	Set.union_eq_iUnion isLindelof_iUnion Bool.countable

IsLindeof

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl_mem_coclosedLindelof_of_isClosed 📖	mathematical	IsLindelof	Set Filter Filter.instMembership Filter.coclosedLindelof Compl.compl Set.instCompl	—	Filter.HasBasis.mem_of_mem hasBasis_coclosedLindelof

IsSigmaCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLindelof 📖	mathematical	IsSigmaCompact	IsLindelof	—	eq_1 IsCompact.isLindelof isLindelof_iUnion instCountableNat

LindelofSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
elim_nhds_subcover 📖	mathematical	Set Filter Filter.instMembership nhds	Set.Countable Set.iUnion Set.instMembership Set.univ	—	IsLindelof.elim_nhds_subcover isLindelof_univ top_unique
isLindelof_univ 📖	mathematical	—	IsLindelof Set.univ	—	—
of_continuous_surjective 📖	mathematical	Continuous	LindelofSpace	—	Set.image_univ_of_surjective IsLindelof.image isLindelof_univ_iff

NonLindelofSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonLindelof_univ 📖	mathematical	—	IsLindelof Set.univ	—	—

Quot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
LindelofSpace 📖	mathematical	—	LindelofSpace instTopologicalSpaceQuot	—	lindelofSpace
lindelofSpace 📖	mathematical	—	LindelofSpace instTopologicalSpaceQuot	—	isLindelof_range

Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
LindelofSpace 📖	mathematical	—	LindelofSpace instTopologicalSpaceQuotient	—	lindelofSpace
lindelofSpace 📖	mathematical	—	LindelofSpace instTopologicalSpaceQuotient	—	Quot.lindelofSpace

SecondCountableTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toHereditarilyLindelof 📖	mathematical	—	HereditarilyLindelofSpace	—	isLindelof_iff_countable_subcover TopologicalSpace.isOpen_iUnion_countable subset_of_subset_of_eq

Set.Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLindelof 📖	mathematical	—	IsLindelof	—	isLindelof_biUnion isLindelof_singleton Set.biUnion_of_singleton
isLindelof_biUnion 📖	mathematical	IsLindelof	Set.iUnion Set Set.instMembership	—	isLindelof_of_countable_subcover subset_trans Set.instIsTransSubset Set.subset_biUnion_of_mem IsLindelof.elim_countable_subcover biUnion_iff Set.iUnion₂_subset Set.iUnion_congr_Prop Set.iUnion_exists Set.biUnion_and' Set.mem_biUnion Function.sometimes_spec
isLindelof_sUnion 📖	mathematical	IsLindelof	Set.sUnion	—	Set.sUnion_eq_biUnion isLindelof_biUnion

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLindelof 📖	mathematical	—	IsLindelof	—	isLindelof_biUnion isLindelof_singleton Set.biUnion_of_singleton
isLindelof_biUnion 📖	mathematical	IsLindelof	Set.iUnion Set Set.instMembership	—	Set.Countable.isLindelof_biUnion countable
isLindelof_sUnion 📖	mathematical	IsLindelof	Set.sUnion	—	Set.sUnion_eq_biUnion isLindelof_biUnion

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLindelof 📖	mathematical	Set.Subsingleton	IsLindelof	—	induction_on isLindelof_empty isLindelof_singleton

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lindelofSpace 📖	mathematical	—	LindelofSpace	—	Set.Subsingleton.isLindelof Set.subsingleton_univ

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLindelof_iff 📖	mathematical	—	IsLindelof instTopologicalSpaceSubtype Set.image	—	Topology.IsEmbedding.isLindelof_iff Topology.IsEmbedding.subtypeVal

Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLindelof_insert_range_of_coLindelof 📖	mathematical	Filter.Tendsto Filter.coLindelof nhds Continuous	IsLindelof Set Set.instInsert Set.range	—	mem_coLindelof Filter.mp_mem Filter.le_principal_iff Filter.univ_mem' Disjoint.le_bot mem_of_mem_nhds Set.mem_image_of_mem IsLindelof.image Set.image_subset_range

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
LindelofSpace 📖	mathematical	Topology.IsClosedEmbedding	LindelofSpace	—	Topology.IsInducing.isLindelof_iff isInducing Set.image_univ IsClosed.isLindelof isClosed_range
isLindelof_preimage 📖	mathematical	Topology.IsClosedEmbedding IsLindelof	Set.preimage	—	Topology.IsInducing.isLindelof_preimage isInducing isClosed_range
nonLindelofSpace 📖	mathematical	Topology.IsClosedEmbedding	NonLindelofSpace	—	nonLindelofSpace_of_neBot Filter.Tendsto.neBot tendsto_coLindelof instNeBotCoLindelofOfNonLindelofSpace
tendsto_coLindelof 📖	mathematical	Topology.IsClosedEmbedding	Filter.Tendsto Filter.coLindelof	—	Filter.HasBasis.tendsto_right_iff hasBasis_coLindelof IsLindelof.compl_mem_coLindelof isLindelof_preimage

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLindelof_iff 📖	mathematical	Topology.IsEmbedding	IsLindelof Set.image	—	Topology.IsInducing.isLindelof_iff isInducing

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLindelof_iff 📖	mathematical	Topology.IsInducing	IsLindelof Set.image	—	IsLindelof.image continuous Filter.map_neBot instCountableInterFilterMap LE.le.trans_eq Filter.map_mono Filter.map_principal mapClusterPt_iff
isLindelof_preimage 📖	mathematical	Topology.IsInducing IsLindelof	Set.preimage	—	IsLindelof.inter_right isLindelof_iff Set.image_preimage_eq_inter_range

(root)

Definitions

Name	Category	Theorems
HereditarilyLindelofSpace 📖	CompData	3 math math: HereditarilyLindelofSpace.of_forall_isOpen, SecondCountableTopology.toHereditarilyLindelof, instHereditarilyLindelofSpaceSubtype
IsHereditarilyLindelof 📖	MathDef	1 math math: HereditarilyLindelofSpace.isHereditarilyLindelof_univ
IsLindelof 📖	MathDef	38 math math: mem_coLindelof', IsHereditarilyLindelof.isLindelof_subset, Tendsto.isLindelof_insert_range_of_coLindelof, isLindelof_iff_isLindelof_univ, isLindelof_iff_lindelofSpace, isLindelof_of_countable_subfamily_closed, hasBasis_coLindelof, isLindelof_singleton, isLindelof_iff_countable_subcover, Set.Subsingleton.isLindelof, isLindelof_iff_LindelofSpace, nonLindelof_univ, mem_coLindelof, isLindelof_of_countable_subcover, hasBasis_coclosedLindelof, HereditarilyLindelof_LindelofSets, isLindelof_empty, mem_coclosedLindelof, IsClosed.isLindelof, Subtype.isLindelof_iff, isLindelof_range, Set.Finite.isLindelof, Topology.IsEmbedding.isLindelof_iff, LindelofSpace.isLindelof_univ, IsLindelof.of_coe, HereditarilyLindelofSpace.isLindelof, isLindelof_univ, NonLindelofSpace.nonLindelof_univ, isLindelof_iff_countable_subfamily_closed, isLindelof_iff_countable, IsCompact.isLindelof, Topology.IsInducing.isLindelof_iff, isLindelof_univ_iff, mem_coclosed_Lindelof', Set.Countable.isLindelof, isLindelof_diagonal, IsHereditarilyLindelof.isLindelof, IsSigmaCompact.isLindelof
LindelofSpace 📖	CompData	17 math math: LindelofSpace.of_continuous_surjective, isLindelof_iff_lindelofSpace, Topology.IsClosedEmbedding.LindelofSpace, not_LindelofSpace_iff, HereditarilyLindelof.to_Lindelof, Countable.LindelofSpace, isLindelof_iff_LindelofSpace, Subsingleton.lindelofSpace, instLindelofSpaceOfCompactSpace, instLindelofSpaceOfSigmaCompactSpace, Quot.LindelofSpace, Quotient.lindelofSpace, Quot.lindelofSpace, lindelofSpace_of_countable_subfamily_closed, Quotient.LindelofSpace, instLindelofSpaceSum, isLindelof_univ_iff
NonLindelofSpace 📖	CompData	4 math math: Filter.coLindelof_neBot_iff, not_LindelofSpace_iff, nonLindelofSpace_of_neBot, Topology.IsClosedEmbedding.nonLindelofSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
HereditarilyLindelof_LindelofSets 📖	mathematical	—	IsLindelof	—	HereditarilyLindelofSpace.isLindelof
cluster_point_of_Lindelof 📖	mathematical	—	ClusterPt	—	isLindelof_univ Filter.principal_univ
coLindelof_le_coclosedLindelof 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.coLindelof Filter.coclosedLindelof	—	iInf_mono le_iInf le_rfl
coLindelof_le_cofinite 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.coLindelof Filter.cofinite	—	IsLindelof.compl_mem_coLindelof Set.Finite.isLindelof compl_compl
countable_cover_nhds 📖	mathematical	Set Filter Filter.instMembership nhds	Set.Countable Set.iUnion Set.instMembership Set.univ	—	countable_cover_nhds_interior Set.univ_subset_iff HasSubset.Subset.trans Set.instIsTransSubset Eq.subset Set.instReflSubset Set.iUnion₂_mono interior_subset
countable_cover_nhds_interior 📖	mathematical	Set Filter Filter.instMembership nhds	Set.Countable Set.iUnion Set.instMembership interior Set.univ	—	IsLindelof.elim_countable_subcover isLindelof_univ isOpen_interior Set.mem_iUnion mem_interior_iff_mem_nhds Set.univ_subset_iff
countable_of_Lindelof_of_discrete 📖	mathematical	—	Countable	—	Set.countable_univ_iff IsLindelof.countable_of_discrete isLindelof_univ
eq_closed_inter_countable 📖	mathematical	IsClosed	Set.Countable Set.iInter Set Set.instMembership	—	compl_inj_iff Set.compl_iInter eq_open_union_countable IsClosed.isOpen_compl
eq_closed_inter_nat 📖	mathematical	IsClosed	Set.iInter	—	compl_inj_iff Set.compl_iInter eq_open_union_nat IsClosed.isOpen_compl
eq_open_union_countable 📖	mathematical	IsOpen	Set.Countable Set.iUnion Set Set.instMembership	—	HereditarilyLindelofSpace.isLindelof IsLindelof.elim_countable_subcover Eq.subset Set.instReflSubset Set.eq_of_subset_of_subset Set.iUnion₂_subset_iUnion
eq_open_union_nat 📖	mathematical	IsOpen	Set.iUnion	—	eq_open_union_countable Set.eq_empty_or_nonempty Set.iUnion_empty Set.iUnion_false Set.iUnion_congr_Prop Set.Countable.exists_eq_range Set.biUnion_range
hasBasis_coLindelof 📖	mathematical	—	Filter.HasBasis Set Filter.coLindelof IsLindelof Compl.compl Set.instCompl	—	Filter.hasBasis_biInf_principal' IsLindelof.union Set.compl_subset_compl Set.subset_union_left Set.subset_union_right isLindelof_empty
hasBasis_coclosedLindelof 📖	mathematical	—	Filter.HasBasis Set Filter.coclosedLindelof IsClosed IsLindelof Compl.compl Set.instCompl	—	iInf_and' Filter.hasBasis_biInf_principal' IsClosed.union IsLindelof.union Set.compl_subset_compl Set.subset_union_left Set.subset_union_right isClosed_empty isLindelof_empty
instHereditarilyLindelofSpaceSubtype 📖	mathematical	—	HereditarilyLindelofSpace instTopologicalSpaceSubtype	—	HereditarilyLindelofSpace.of_forall_isOpen Subtype.isLindelof_iff HereditarilyLindelofSpace.isLindelof
instLindelofSpaceOfCompactSpace 📖	mathematical	—	LindelofSpace	—	IsCompact.isLindelof isCompact_univ
instLindelofSpaceOfSigmaCompactSpace 📖	mathematical	—	LindelofSpace	—	IsSigmaCompact.isLindelof isSigmaCompact_univ
instLindelofSpaceSigmaOfCountable 📖	mathematical	LindelofSpace	instTopologicalSpaceSigma	—	Set.Sigma.univ isLindelof_iUnion isLindelof_range continuous_sigmaMk
instLindelofSpaceSum 📖	mathematical	—	LindelofSpace instTopologicalSpaceSum	—	Set.range_inl_union_range_inr IsLindelof.union isLindelof_range continuous_inl continuous_inr
instNeBotCoLindelofOfNonLindelofSpace 📖	mathematical	—	Filter.NeBot Filter.coLindelof	—	Filter.HasBasis.neBot_iff hasBasis_coLindelof Mathlib.Tactic.Contrapose.contrapose₁ Set.compl_empty_iff Set.not_nonempty_iff_eq_empty nonLindelof_univ
instNeBotCoclosedLindelofOfNonLindelofSpace 📖	mathematical	—	Filter.NeBot Filter.coclosedLindelof	—	Filter.neBot_of_le instNeBotCoLindelofOfNonLindelofSpace coLindelof_le_coclosedLindelof
isLindelof_accumulate 📖	mathematical	IsLindelof	Set.accumulate	—	Set.Finite.isLindelof_biUnion Set.finite_le_nat
isLindelof_diagonal 📖	mathematical	—	IsLindelof instTopologicalSpaceProd Set.diagonal	—	isLindelof_range Continuous.prodMk continuous_id Set.range_diag
isLindelof_empty 📖	mathematical	—	IsLindelof Set Set.instEmptyCollection	—	Filter.NeBot.ne Filter.empty_mem_iff_bot Filter.le_principal_iff
isLindelof_iUnion 📖	mathematical	IsLindelof	Set.iUnion	—	Set.Countable.isLindelof_sUnion Set.countable_range Set.forall_mem_range
isLindelof_iff_LindelofSpace 📖	mathematical	—	IsLindelof LindelofSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	isLindelof_iff_lindelofSpace
isLindelof_iff_countable 📖	mathematical	—	IsLindelof Set.Countable	—	IsLindelof.countable_of_discrete Set.Countable.isLindelof
isLindelof_iff_countable_subcover 📖	mathematical	—	IsLindelof Set.Countable Set Set.instHasSubset Set.iUnion Set.instMembership	—	IsLindelof.elim_countable_subcover isLindelof_of_countable_subcover
isLindelof_iff_countable_subfamily_closed 📖	mathematical	—	IsLindelof Set.Countable Set Set.instInter Set.iInter Set.instMembership Set.instEmptyCollection	—	IsLindelof.elim_countable_subfamily_closed isLindelof_of_countable_subfamily_closed
isLindelof_iff_isLindelof_univ 📖	mathematical	—	IsLindelof Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.univ	—	Subtype.isLindelof_iff Set.image_univ Subtype.range_coe
isLindelof_iff_lindelofSpace 📖	mathematical	—	IsLindelof LindelofSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	isLindelof_iff_isLindelof_univ isLindelof_univ_iff
isLindelof_of_countable_subcover 📖	mathematical	Set.Countable Set Set.instHasSubset Set.iUnion Set.instMembership	IsLindelof	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq Mathlib.Tactic.Push.not_forall_eq Set.mem_iUnion Filter.sets_of_superset Filter.le_principal_iff Filter.HasBasis.disjoint_iff_left nhds_basis_opens countable_bInter_mem Filter.compl_notMem Set.compl_iUnion₂ compl_compl
isLindelof_of_countable_subfamily_closed 📖	mathematical	Set.Countable Set Set.instInter Set.iInter Set.instMembership Set.instEmptyCollection	IsLindelof	—	isLindelof_of_countable_subcover IsOpen.isClosed_compl disjoint_iff Set.compl_iUnion Set.disjoint_compl_right_iff_subset Set.compl_iUnion₂
isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis 📖	mathematical	TopologicalSpace.IsTopologicalBasis Set.range Set IsLindelof	IsOpen Set.Countable Set.iUnion Set.instMembership	—	TopologicalSpace.IsTopologicalBasis.open_eq_iUnion IsLindelof.elim_countable_subcover TopologicalSpace.IsTopologicalBasis.isOpen Set.mem_range_self Set.Subset.rfl Set.Countable.image le_antisymm Set.Subset.trans Set.iUnion_subtype Set.subset_iUnion Set.mem_image_of_mem Set.iUnion₂_subset Set.mem_image Set.Countable.isLindelof_biUnion isOpen_biUnion
isLindelof_range 📖	mathematical	Continuous	IsLindelof Set.range	—	Set.image_univ IsLindelof.image isLindelof_univ
isLindelof_singleton 📖	mathematical	—	IsLindelof Set Set.instSingletonSet	—	ClusterPt.of_le_nhds' LE.le.trans Filter.principal_singleton pure_le_nhds
isLindelof_univ 📖	mathematical	—	IsLindelof Set.univ	—	LindelofSpace.isLindelof_univ
isLindelof_univ_iff 📖	mathematical	—	IsLindelof Set.univ LindelofSpace	—	LindelofSpace.isLindelof_univ
lindelofSpace_of_countable_subfamily_closed 📖	mathematical	Set.Countable Set.iInter Set Set.instMembership Set.instEmptyCollection	LindelofSpace	—	isLindelof_of_countable_subfamily_closed Set.univ_inter
mem_coLindelof 📖	mathematical	—	Set Filter Filter.instMembership Filter.coLindelof IsLindelof Set.instHasSubset Compl.compl Set.instCompl	—	Filter.HasBasis.mem_iff hasBasis_coLindelof
mem_coLindelof' 📖	mathematical	—	Set Filter Filter.instMembership Filter.coLindelof IsLindelof Set.instHasSubset Compl.compl Set.instCompl	—	mem_coLindelof Set.compl_subset_comm
mem_coclosedLindelof 📖	mathematical	—	Set Filter Filter.instMembership Filter.coclosedLindelof IsClosed IsLindelof Set.instHasSubset Compl.compl Set.instCompl	—	Filter.HasBasis.mem_iff hasBasis_coclosedLindelof
mem_coclosed_Lindelof' 📖	mathematical	—	Set Filter Filter.instMembership Filter.coclosedLindelof IsClosed IsLindelof Set.instHasSubset Compl.compl Set.instCompl	—	—
nonLindelofSpace_of_neBot 📖	mathematical	—	NonLindelofSpace	—	Set.Nonempty.ne_empty Filter.nonempty_of_mem IsLindelof.compl_mem_coLindelof Set.compl_univ
nonLindelof_univ 📖	mathematical	—	IsLindelof Set.univ	—	NonLindelofSpace.nonLindelof_univ
not_LindelofSpace_iff 📖	mathematical	—	LindelofSpace NonLindelofSpace	—	—

---

← Back to Index