Bases

📁 Source: Mathlib/Topology/Bases.lean

Statistics

Metric	Count
Definitions FirstCountableTopology, SecondCountableTopology, IsSeparable, IsTopologicalBasis, SeparableSpace, countableBasis, denseSeq, encodableCountableBasis	8
Theorems exists_countable_dense_subset, exists_countable_dense_subset_bot_top, isSeparable_iff, separableSpace, separableSpace', toSecondCountableTopology, nhds_generated_countable, separableSpace_of_injective, separableSpace_of_isInducing, iInf, iInf_induced, countable_of_isOpen_disjoint, is_open_generated_countable, isSeparable, isSeparable, countable_of_isOpen, countable_of_nonempty_interior, to_separableSpace, tendsto_subseq, closure, iUnion, image, mono, of_separableSpace, of_subtype, prod, union, univ_pi, continuous_iff, dense_iff, diff_empty, eq_generateFrom, eq_of_forall_subset_iff, exists_countable, exists_countable_biUnion_of_isOpen, exists_nonempty_subset, exists_subset_inter, exists_subset_of_mem_open, induced, inf, inf_induced, insert_empty, isInducing, isOpen, isOpenMap_iff, isOpen_iff, isOpen_induction, isQuotientMap, mem_closure_iff, mem_nhds, mem_nhds_iff, nhds_hasBasis, of_hasBasis_nhds, of_isOpen_of_subset, open_eq_iUnion, open_eq_sUnion, open_eq_sUnion', open_iff_eq_sUnion, prod, quotient, sUnion_eq, secondCountableTopology, sigma, subset_of_forall_subset, sum, secondCountableTopology, mk', to_firstCountableTopology, to_separableSpace, exists_countable_dense, of_denseRange, firstCountableTopology, secondCountableTopology, countable_countableBasis, countable_cover_nhds, countable_cover_nhdsWithin, denseRange_denseSeq, empty_notMem_countableBasis, eq_generateFrom_countableBasis, exists_countable_basis, exists_countable_dense, exists_countable_of_generateFrom, exists_dense_seq, firstCountableTopology_induced, instFirstCountableTopologyForallOfCountable, instFirstCountableTopologyProd, instSecondCountableTopologyForallOfCountable, instSecondCountableTopologyOfCountableOfFirstCountableTopology, instSecondCountableTopologyProd, instSecondCountableTopologySigmaOfCountable, instSecondCountableTopologySum, instSeparableSpaceForallOfCountable, instSeparableSpaceProd, instSeparableSpaceQuot, instSeparableSpaceQuotient, instSeparableSpaceSum, isBasis_countableBasis, isCountablyGenerated_nhdsWithin, isOpen_biUnion_countable, isOpen_iUnion_countable, isOpen_of_mem_countableBasis, isOpen_sUnion_countable, isSeparable_closure, isSeparable_iUnion, isSeparable_pi, isSeparable_range, isSeparable_union, isSeparable_univ_iff, isTopologicalBasis_empty, isTopologicalBasis_of_cover, isTopologicalBasis_of_isOpen_of_nhds, isTopologicalBasis_of_subbasis, isTopologicalBasis_of_subbasis_of_finiteInter, isTopologicalBasis_of_subbasis_of_inter, isTopologicalBasis_opens, nonempty_of_mem_countableBasis, secondCountableTopology_iInf, secondCountableTopology_induced, secondCountableTopology_of_countable_cover, separableSpace_iff, separableSpace_iff_countable, separableSpace_sum_iff, firstCountableTopology, secondCountableTopology, separableSpace, firstCountableTopology, secondCountableTopology, separableSpace, secondCountableTopology, separableSpace, exists_countable_dense_bot_top, isOpenMap_eval, isTopologicalBasis_pi, isTopologicalBasis_singletons, isTopologicalBasis_subtype, separableSpace_univ	136
Total	144

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_countable_dense_subset 📖	mathematical	Dense	Set Set.instHasSubset Set.Countable	—	TopologicalSpace.exists_countable_dense Subtype.coe_image_subset Set.Countable.image DenseRange.dense_image denseRange_val continuous_subtype_val
exists_countable_dense_subset_bot_top 📖	mathematical	Dense	Set Set.instHasSubset Set.Countable Set.instMembership	—	exists_countable_dense_subset Set.inter_subset_right Set.Countable.mono Set.inter_subset_left Set.Countable.union Set.countable_isBot Set.countable_isTop mono Set.subset_inter Set.subset_union_left
isSeparable_iff 📖	mathematical	Dense	TopologicalSpace.IsSeparable TopologicalSpace.SeparableSpace	—	closure_eq IsClosed.closure_subset_iff isClosed_closure

DenseRange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
separableSpace 📖	mathematical	DenseRange Continuous	TopologicalSpace.SeparableSpace	—	TopologicalSpace.exists_countable_dense Set.Countable.image dense_image
separableSpace' 📖	mathematical	DenseRange	TopologicalSpace.SeparableSpace	—	TopologicalSpace.SeparableSpace.of_denseRange

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toSecondCountableTopology 📖	mathematical	—	SecondCountableTopology	—	Set.to_countable SetCoe.countable to_countable Set.instFinite TopologicalSpace.IsTopologicalBasis.eq_generateFrom TopologicalSpace.isTopologicalBasis_opens

FirstCountableTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nhds_generated_countable 📖	mathematical	—	Filter.IsCountablyGenerated nhds	—	—

IsOpenMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
separableSpace_of_injective 📖	mathematical	IsOpenMap	TopologicalSpace.SeparableSpace	—	TopologicalSpace.exists_countable_dense Set.Countable.preimage Dense.preimage
separableSpace_of_isInducing 📖	mathematical	IsOpenMap Topology.IsInducing	TopologicalSpace.SeparableSpace	—	isEmpty_or_nonempty TopologicalSpace.Countable.to_separableSpace Encodable.countable TopologicalSpace.exists_countable_dense Set.Countable.image Topology.IsInducing.dense_iff Dense.inter_open_nonempty IsOpen.inter isOpen_range Set.mem_range_self Function.apply_invFun_apply Set.mem_image_of_mem

IsTopologicalBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iInf 📖	mathematical	TopologicalSpace.IsTopologicalBasis	iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice setOf Set Finset Set.iInter Finset.instMembership	—	TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds isOpen_biInter_finset IsOpen.mono TopologicalSpace.IsTopologicalBasis.isOpen iInf_le Filter.HasBasis.mem_iff Filter.HasBasis.iInf' TopologicalSpace.IsTopologicalBasis.nhds_hasBasis nhds_iInf IsOpen.mem_nhds Set.iInter_congr_Prop
iInf_induced 📖	mathematical	TopologicalSpace.IsTopologicalBasis	iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice TopologicalSpace.induced setOf Set Finset Set.iInter Finset.instMembership Set.preimage	—	Set.mem_image_of_mem Set.iInter₂_congr Function.sometimes_spec iInf TopologicalSpace.IsTopologicalBasis.induced

Pairwise

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable_of_isOpen_disjoint 📖	mathematical	Pairwise Function.onFun Set Disjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice IsOpen Set.Nonempty	Countable	—	TopologicalSpace.exists_countable_dense eq Set.not_disjoint_iff Set.Countable.to_subtype Function.Injective.countable Function.Injective.codRestrict Dense.exists_mem_open

SecondCountableTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
is_open_generated_countable 📖	mathematical	—	Set.Countable Set TopologicalSpace.generateFrom	—	—

Set.Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparable 📖	mathematical	—	TopologicalSpace.IsSeparable	—	subset_closure

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparable 📖	mathematical	—	TopologicalSpace.IsSeparable	—	Set.Countable.isSeparable countable

Set.PairwiseDisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable_of_isOpen 📖	mathematical	Set.PairwiseDisjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice IsOpen Set.Nonempty	Set.Countable	—	Pairwise.countable_of_isOpen_disjoint Set.Pairwise.subtype
countable_of_nonempty_interior 📖	mathematical	Set.PairwiseDisjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.Nonempty interior	Set.Countable	—	countable_of_isOpen mono interior_subset isOpen_interior

TopologicalSpace

Definitions

Name	Category	Theorems
IsSeparable 📖	MathDef	19 math math: isSeparable_range_derivWithin, isSeparable_union, MeasureTheory.StronglyMeasurable.isSeparable_range, TotallyBounded.isSeparable, Dense.isSeparable_iff, aestronglyMeasurable_iff_aemeasurable_separable, stronglyMeasurable_iff_measurable_separable, IsSeparable.of_subtype, IsCompact.isSeparable, isSeparable_iUnion, IsSeparable.of_separableSpace, isSeparable_range_deriv, Set.Countable.isSeparable, Set.Finite.isSeparable, isSeparable_closure, isSeparable_univ_iff, aestronglyMeasurable_iff_nullMeasurable_separable, MeasureTheory.AEStronglyMeasurable.isSeparable_ae_range, isSeparable_range
IsTopologicalBasis 📖	CompData	37 math math: IsTopologicalBasis.of_hasBasis_nhds, CompletelyRegularSpace.isTopologicalBasis_clopens_of_cardinalMk_lt_continuum, AlgebraicGeometry.Scheme.affineBasisCover_is_basis, MeasureTheory.Measure.isTopologicalBasis_isOpen_lt_top, PrimitiveSpectrum.isTopologicalBasis_relativeLower, CompleteType.isTopologicalBasis_range_typesWith, PiNat.isTopologicalBasis_cylinders, Topology.IsUpper.isTopologicalBasis_insert_univ_subbasis, isTopologicalBasis_of_subbasis_of_inter, Ctop.Realizer.is_basis, isTopologicalBasis_of_isOpen_of_nhds, isTopologicalBasis_opens, Real.isTopologicalBasis_Ioo_rat, Topology.IsLower.isTopologicalBasis, loc_compact_Haus_tot_disc_of_zero_dim, ultrafilterBasis_is_basis, isTopologicalBasis_isClopen, PrespectralSpace.isTopologicalBasis, Topology.IsUpper.isTopologicalBasis, locallyConnectedSpace_iff_isTopologicalBasis_isOpen_isPreconnected, PrimeSpectrum.isTopologicalBasis_basic_opens, isTopologicalBasis_empty, isTopologicalBasis_singletons, IsTopologicalBasis.isOpen_isPreconnected, exists_countable_basis, prespectralSpace_iff, isTopologicalBasis_of_subbasis, ProjectiveSpectrum.isTopologicalBasis_basic_opens, isTopologicalBasis_clopens, isTopologicalBasis_biInter_Ioi_Iio_of_generateFrom, Ctop.toTopsp_isTopologicalBasis, isBasis_countableBasis, Filter.isTopologicalBasis_Iic_principal, IsLocalHomeomorph.isTopologicalBasis, Topology.IsLower.isTopologicalBasis_insert_univ_subbasis, isTopologicalBasis_of_subbasis_of_finiteInter, Topology.IsLawson.isTopologicalBasis
SeparableSpace 📖	CompData	29 math math: instSeparableSpaceQuot, instSeparableSpaceOrderDual, DomMulAct.instSeparableSpace, Dense.isSeparable_iff, UniformSpace.Completion.separableSpace_completion, MeasureTheory.StronglyMeasurable.separableSpace_range_union_singleton, Topology.IsQuotientMap.separableSpace, Topology.IsEmbedding.separableSpace, DenseRange.separableSpace, instSeparableSpaceSum, instSeparableSpaceProd, separableSpace_univ, IsSeparable.separableSpace, instSeparableSpaceQuotient, Topology.IsOpenEmbedding.separableSpace, IsOpenMap.separableSpace_of_isInducing, IsDenseInducing.separableSpace, isSeparable_univ_iff, IsOpenMap.separableSpace_of_injective, DomAddAct.instSeparableSpace, SeparableSpace.of_denseRange, SecondCountableTopology.to_separableSpace, separableSpace_sum_iff, separableSpace_iff, DenseRange.separableSpace', Countable.to_separableSpace, separableSpace_iff_countable, ContinuousMap.instSeparableSpace, IsDenseEmbedding.separableSpace
countableBasis 📖	CompOp	4 math math: countable_countableBasis, empty_notMem_countableBasis, isBasis_countableBasis, eq_generateFrom_countableBasis
denseSeq 📖	CompOp	1 math math: denseRange_denseSeq
encodableCountableBasis 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable_countableBasis 📖	mathematical	—	Set.Countable Set countableBasis	—	exists_countable_basis
countable_cover_nhds 📖	mathematical	Set Filter Filter.instMembership nhds	Set.Countable Set.iUnion Set.instMembership Set.univ	—	isOpen_iUnion_countable isOpen_interior mem_interior_iff_mem_nhds Set.eq_univ_of_subset Set.iUnion₂_mono interior_subset
countable_cover_nhdsWithin 📖	mathematical	Set Filter Filter.instMembership nhdsWithin	Set.instHasSubset Set.Countable Set.iUnion Set.instMembership	—	preimage_coe_mem_nhds_subtype countable_cover_nhds Subtype.secondCountableTopology Subtype.coe_image_subset Set.Countable.image Set.biUnion_image
denseRange_denseSeq 📖	mathematical	—	DenseRange denseSeq	—	exists_dense_seq
empty_notMem_countableBasis 📖	mathematical	—	Set Set.instMembership countableBasis Set.instEmptyCollection	—	exists_countable_basis
eq_generateFrom_countableBasis 📖	mathematical	—	generateFrom countableBasis	—	IsTopologicalBasis.eq_generateFrom isBasis_countableBasis
exists_countable_basis 📖	mathematical	—	Set.Countable Set Set.instMembership Set.instEmptyCollection IsTopologicalBasis	—	SecondCountableTopology.is_open_generated_countable Set.Countable.mono Set.diff_subset Set.Countable.image Set.countable_setOf_finite_subset Set.notMem_diff_of_mem IsTopologicalBasis.diff_empty isTopologicalBasis_of_subbasis
exists_countable_dense 📖	mathematical	—	Set.Countable Dense	—	SeparableSpace.exists_countable_dense
exists_countable_of_generateFrom 📖	mathematical	generateFrom	Set Set.instHasSubset Set.Countable	—	isTopologicalBasis_of_subbasis IsTopologicalBasis.exists_countable Set.Countable.biUnion Set.Finite.countable le_antisymm le_generateFrom_iff_subset_isOpen isOpen_generateFrom_of_mem IsTopologicalBasis.eq_generateFrom Set.sInter_eq_biInter Set.Finite.isOpen_biInter Function.sometimes_spec
exists_dense_seq 📖	mathematical	—	DenseRange	—	exists_countable_dense Set.countable_iff_exists_subset_range Dense.mono
firstCountableTopology_induced 📖	mathematical	—	FirstCountableTopology induced	—	Filter.comap.isCountablyGenerated FirstCountableTopology.nhds_generated_countable nhds_induced
instFirstCountableTopologyForallOfCountable 📖	mathematical	FirstCountableTopology	Pi.topologicalSpace	—	nhds_pi Filter.pi.isCountablyGenerated FirstCountableTopology.nhds_generated_countable
instFirstCountableTopologyProd 📖	mathematical	—	FirstCountableTopology instTopologicalSpaceProd	—	nhds_prod_eq Filter.prod.isCountablyGenerated FirstCountableTopology.nhds_generated_countable
instSecondCountableTopologyForallOfCountable 📖	mathematical	SecondCountableTopology	Pi.topologicalSpace	—	secondCountableTopology_iInf secondCountableTopology_induced
instSecondCountableTopologyOfCountableOfFirstCountableTopology 📖	mathematical	—	SecondCountableTopology	—	Set.countable_range instCountableProd instCountableNat le_antisymm le_generateFrom_iff_subset_isOpen le_iff_nhds Filter.HasBasis.ge_iff Filter.HasAntitoneBasis.toHasBasis IsOpen.mem_nhds isOpen_generateFrom_of_mem Filter.HasBasis.exists_antitone_subbasis FirstCountableTopology.nhds_generated_countable nhds_basis_opens
instSecondCountableTopologyProd 📖	mathematical	—	SecondCountableTopology instTopologicalSpaceProd	—	IsTopologicalBasis.secondCountableTopology IsTopologicalBasis.prod isBasis_countableBasis Set.Countable.image2 countable_countableBasis
instSecondCountableTopologySigmaOfCountable 📖	mathematical	SecondCountableTopology	instTopologicalSpaceSigma	—	IsTopologicalBasis.sigma isBasis_countableBasis Set.countable_iUnion Set.Countable.image countable_countableBasis IsTopologicalBasis.secondCountableTopology
instSecondCountableTopologySum 📖	mathematical	—	SecondCountableTopology instTopologicalSpaceSum	—	IsTopologicalBasis.sum isBasis_countableBasis Set.Countable.union Set.Countable.image countable_countableBasis IsTopologicalBasis.secondCountableTopology
instSeparableSpaceForallOfCountable 📖	mathematical	SeparableSpace	Pi.topologicalSpace	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Countable.to_separableSpace Finite.to_countable Finite.of_subsingleton Nontrivial.to_nonempty Set.countable_range instCountableSigma Finset.countable instCountableForallOfFinite Finite.of_fintype Set.Countable.to_subtype dense_iff_inter_open isOpen_pi_iff Dense.exists_mem_open CanLift.prf Pi.canLift Subtype.canLift Set.mem_range_self exists_countable_dense
instSeparableSpaceProd 📖	mathematical	—	SeparableSpace instTopologicalSpaceProd	—	exists_countable_dense Set.Countable.prod Dense.prod
instSeparableSpaceQuot 📖	mathematical	—	SeparableSpace instTopologicalSpaceQuot	—	Topology.IsQuotientMap.separableSpace
instSeparableSpaceQuotient 📖	mathematical	—	SeparableSpace instTopologicalSpaceQuotient	—	Topology.IsQuotientMap.separableSpace
instSeparableSpaceSum 📖	mathematical	—	SeparableSpace instTopologicalSpaceSum	—	exists_countable_dense Set.Countable.union Set.Countable.image closure_union Topology.IsClosedEmbedding.closure_image_eq Topology.IsClosedEmbedding.inl Dense.closure_eq Topology.IsClosedEmbedding.inr Set.image_univ Set.range_inl_union_range_inr
isBasis_countableBasis 📖	mathematical	—	IsTopologicalBasis countableBasis	—	exists_countable_basis
isCountablyGenerated_nhdsWithin 📖	mathematical	—	Filter.IsCountablyGenerated nhdsWithin	—	Filter.Inf.isCountablyGenerated Filter.isCountablyGenerated_principal
isOpen_biUnion_countable 📖	mathematical	IsOpen	Set Set.instHasSubset Set.Countable Set.iUnion Set.instMembership	—	Set.biUnion_image isOpen_iUnion_countable Set.Countable.image Set.iUnion_subtype
isOpen_iUnion_countable 📖	mathematical	IsOpen	Set.Countable Set.iUnion Set Set.instMembership	—	Set.countable_range Set.Countable.to_subtype Set.Countable.mono Set.sep_subset countable_countableBasis HasSubset.Subset.antisymm Set.instAntisymmSubset Set.iUnion₂_subset_iUnion Set.sUnion_subset IsTopologicalBasis.exists_subset_of_mem_open isBasis_countableBasis
isOpen_of_mem_countableBasis 📖	mathematical	Set Set.instMembership countableBasis	IsOpen	—	IsTopologicalBasis.isOpen isBasis_countableBasis
isOpen_sUnion_countable 📖	mathematical	IsOpen	Set.Countable Set Set.instHasSubset Set.sUnion	—	Set.sUnion_eq_biUnion isOpen_biUnion_countable
isSeparable_closure 📖	mathematical	—	IsSeparable closure	—	IsClosed.closure_subset_iff isClosed_closure
isSeparable_iUnion 📖	mathematical	—	IsSeparable Set.iUnion	—	IsSeparable.mono Set.subset_iUnion IsSeparable.iUnion
isSeparable_pi 📖	mathematical	IsSeparable	Pi.topologicalSpace setOf	—	IsSeparable.univ_pi
isSeparable_range 📖	mathematical	Continuous	IsSeparable Set.range	—	IsSeparable.image isSeparable_univ_iff Set.image_univ
isSeparable_union 📖	mathematical	—	IsSeparable Set Set.instUnion	—	Set.union_eq_iUnion Bool.countable
isSeparable_univ_iff 📖	mathematical	—	IsSeparable Set.univ SeparableSpace	—	Dense.isSeparable_iff dense_univ
isTopologicalBasis_empty 📖	mathematical	—	IsTopologicalBasis Set Set.instEmptyCollection IsEmpty	—	Set.sUnion_empty IsTopologicalBasis.sUnion_eq Set.univ_eq_empty_iff Unique.instSubsingleton IsEmpty.instSubsingleton
isTopologicalBasis_of_cover 📖	mathematical	IsOpen Set.iUnion Set.univ IsTopologicalBasis Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	Set.image	—	isTopologicalBasis_of_isOpen_of_nhds IsOpen.isOpenMap_subtype_val IsTopologicalBasis.isOpen Set.iUnion_eq_univ_iff CanLift.prf Subtype.canLift IsTopologicalBasis.exists_subset_of_mem_open IsOpen.preimage continuous_subtype_val Set.mem_iUnion Set.mem_image_of_mem Set.image_subset_iff
isTopologicalBasis_of_isOpen_of_nhds 📖	mathematical	IsOpen Set Set.instMembership Set.instHasSubset	IsTopologicalBasis	—	IsTopologicalBasis.of_hasBasis_nhds Filter.HasBasis.to_hasBasis' nhds_basis_opens IsOpen.mem_nhds
isTopologicalBasis_of_subbasis 📖	mathematical	generateFrom	IsTopologicalBasis Set.image Set Set.sInter setOf Set.Finite Set.instHasSubset	—	Set.Finite.union Set.union_subset Set.sInter_union Set.Subset.rfl Set.sUnion_image Set.iUnion₂_eq_univ_iff Set.finite_empty Set.empty_subset Set.sInter_empty Set.mem_univ le_antisymm le_generateFrom Set.Finite.isOpen_sInter generateFrom_anti Set.sInter_singleton Set.finite_singleton Set.singleton_subset_iff
isTopologicalBasis_of_subbasis_of_finiteInter 📖	mathematical	generateFrom FiniteInter	IsTopologicalBasis	—	le_antisymm Set.sInter_singleton CanLift.prf Set.instCanLiftFinsetCoeFinite FiniteInter.finiteInter_mem isTopologicalBasis_of_subbasis
isTopologicalBasis_of_subbasis_of_inter 📖	mathematical	generateFrom Set Set.instMembership Set.instInter	IsTopologicalBasis Set.instInsert Set.univ	—	isTopologicalBasis_of_subbasis_of_finiteInter generateFrom_insert_univ FiniteInter.mk₂
isTopologicalBasis_opens 📖	mathematical	—	IsTopologicalBasis setOf Set IsOpen	—	isTopologicalBasis_of_isOpen_of_nhds
nonempty_of_mem_countableBasis 📖	mathematical	Set Set.instMembership countableBasis	Set.Nonempty	—	Set.nonempty_iff_ne_empty empty_notMem_countableBasis
secondCountableTopology_iInf 📖	mathematical	SecondCountableTopology	iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	eq_generateFrom_countableBasis generateFrom_iUnion SecondCountableTopology.mk' Set.countable_iUnion countable_countableBasis
secondCountableTopology_induced 📖	mathematical	—	SecondCountableTopology induced	—	SecondCountableTopology.is_open_generated_countable Set.Countable.image induced_generateFrom_eq
secondCountableTopology_of_countable_cover 📖	—	SecondCountableTopology Set.Elem instTopologicalSpaceSubtype Set Set.instMembership IsOpen Set.iUnion Set.univ	—	—	IsTopologicalBasis.secondCountableTopology isTopologicalBasis_of_cover isBasis_countableBasis Set.countable_iUnion Set.Countable.image countable_countableBasis
separableSpace_iff 📖	mathematical	—	SeparableSpace Set.Countable Dense	—	—
separableSpace_iff_countable 📖	mathematical	—	SeparableSpace Countable	—	—
separableSpace_sum_iff 📖	mathematical	—	SeparableSpace instTopologicalSpaceSum	—	Topology.IsOpenEmbedding.separableSpace Topology.IsOpenEmbedding.inl Topology.IsOpenEmbedding.inr instSeparableSpaceSum

TopologicalSpace.Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_separableSpace 📖	mathematical	—	TopologicalSpace.SeparableSpace	—	Set.countable_univ dense_univ

TopologicalSpace.FirstCountableTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_subseq 📖	mathematical	—	StrictMono Nat.instPreorder Filter.Tendsto Filter.atTop nhds	—	Filter.subseq_tendsto_of_neBot FirstCountableTopology.nhds_generated_countable

TopologicalSpace.IsSeparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	mathematical	TopologicalSpace.IsSeparable	closure	—	TopologicalSpace.isSeparable_closure
iUnion 📖	mathematical	TopologicalSpace.IsSeparable	Set.iUnion	—	Set.countable_iUnion Set.iUnion_subset_iff HasSubset.Subset.trans Set.instIsTransSubset closure_mono Set.subset_iUnion
image 📖	mathematical	TopologicalSpace.IsSeparable Continuous	Set.image	—	Set.Countable.image Set.image_subset_iff HasSubset.Subset.trans Set.instIsTransSubset closure_subset_preimage_closure_image
mono 📖	—	TopologicalSpace.IsSeparable Set Set.instHasSubset	—	—	HasSubset.Subset.trans Set.instIsTransSubset
of_separableSpace 📖	mathematical	—	TopologicalSpace.IsSeparable	—	mono TopologicalSpace.isSeparable_univ_iff Set.subset_univ
of_subtype 📖	mathematical	—	TopologicalSpace.IsSeparable	—	Subtype.range_coe_subtype TopologicalSpace.isSeparable_range continuous_subtype_val
prod 📖	mathematical	TopologicalSpace.IsSeparable	instTopologicalSpaceProd SProd.sprod Set Set.instSProd	—	Set.Countable.prod closure_prod_eq Set.prod_mono
union 📖	mathematical	TopologicalSpace.IsSeparable	Set Set.instUnion	—	TopologicalSpace.isSeparable_union
univ_pi 📖	mathematical	TopologicalSpace.IsSeparable	Pi.topologicalSpace Set.pi Set.univ	—	Set.eq_empty_or_nonempty Set.Countable.isSeparable Set.countable_empty Set.countable_range instCountableSigma Finset.countable instCountableForallOfFinite Finite.of_fintype Set.Countable.to_subtype mem_closure_iff isOpen_pi_iff Set.mem_range_self

TopologicalSpace.IsTopologicalBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_iff 📖	mathematical	TopologicalSpace.IsTopologicalBasis	Continuous IsOpen Set.preimage	—	eq_generateFrom continuous_generateFrom_iff
dense_iff 📖	mathematical	TopologicalSpace.IsTopologicalBasis	Dense Set.Nonempty Set Set.instInter	—	mem_closure_iff
diff_empty 📖	mathematical	TopologicalSpace.IsTopologicalBasis	Set Set.instSDiff Set.instSingletonSet Set.instEmptyCollection	—	TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds isOpen isOpen_iff Set.notMem_empty
eq_generateFrom 📖	mathematical	TopologicalSpace.IsTopologicalBasis	TopologicalSpace.generateFrom	—	—
eq_of_forall_subset_iff 📖	—	TopologicalSpace.IsTopologicalBasis IsOpen Set Set.instHasSubset	—	—	open_eq_sUnion' Set.ext
exists_countable 📖	mathematical	TopologicalSpace.IsTopologicalBasis	Set Set.instHasSubset Set.Countable	—	exists_countable_biUnion_of_isOpen isOpen TopologicalSpace.isBasis_countableBasis Set.Countable.biUnion TopologicalSpace.countable_countableBasis TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds isOpen_iff Set.Subset.trans Set.subset_iUnion₂_of_subset Set.Subset.refl Eq.subset Set.instReflSubset Function.sometimes_spec
exists_countable_biUnion_of_isOpen 📖	mathematical	TopologicalSpace.IsTopologicalBasis IsOpen	Set Set.instHasSubset Set.Countable Set.iUnion Set.instMembership	—	exists_subset_of_mem_open TopologicalSpace.isOpen_iUnion_countable isOpen Set.Countable.image Set.biUnion_image Set.Subset.antisymm Set.iUnion_coe_set Set.iUnion_congr_Prop Function.sometimes_spec
exists_nonempty_subset 📖	mathematical	TopologicalSpace.IsTopologicalBasis Set.Nonempty IsOpen	Set Set.instMembership Set.instHasSubset	—	exists_subset_of_mem_open
exists_subset_inter 📖	mathematical	TopologicalSpace.IsTopologicalBasis Set Set.instMembership Set.instInter	Set.instHasSubset	—	—
exists_subset_of_mem_open 📖	mathematical	TopologicalSpace.IsTopologicalBasis Set Set.instMembership IsOpen	Set.instHasSubset	—	mem_nhds_iff IsOpen.mem_nhds
induced 📖	mathematical	TopologicalSpace.IsTopologicalBasis	TopologicalSpace.induced Set.image Set Set.preimage	—	isInducing Topology.IsInducing.induced
inf 📖	mathematical	TopologicalSpace.IsTopologicalBasis	TopologicalSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice Set.image2 Set Set.instInter	—	of_hasBasis_nhds nhds_inf Filter.HasBasis.to_image_id Filter.HasBasis.inf nhds_hasBasis
inf_induced 📖	mathematical	TopologicalSpace.IsTopologicalBasis	TopologicalSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice TopologicalSpace.induced Set.image2 Set Set.instInter Set.preimage	—	Set.image2_image_right Set.image2_image_left inf induced
insert_empty 📖	mathematical	TopologicalSpace.IsTopologicalBasis	Set Set.instInsert Set.instEmptyCollection	—	of_isOpen_of_subset isOpen_empty isOpen Set.subset_insert
isInducing 📖	mathematical	Topology.IsInducing TopologicalSpace.IsTopologicalBasis	Set.image Set Set.preimage	—	of_hasBasis_nhds Set.image_congr Filter.HasBasis.to_image_id Topology.IsInducing.basis_nhds nhds_hasBasis
isOpen 📖	mathematical	TopologicalSpace.IsTopologicalBasis Set Set.instMembership	IsOpen	—	eq_generateFrom
isOpenMap_iff 📖	mathematical	TopologicalSpace.IsTopologicalBasis	IsOpenMap IsOpen Set.image	—	isOpen open_eq_sUnion' Set.sUnion_eq_iUnion Set.image_iUnion isOpen_iUnion
isOpen_iff 📖	mathematical	TopologicalSpace.IsTopologicalBasis	IsOpen Set Set.instMembership Set.instHasSubset	—	mem_nhds_iff
isOpen_induction 📖	—	TopologicalSpace.IsTopologicalBasis Set.sUnion IsOpen	—	—	open_eq_sUnion
isQuotientMap 📖	mathematical	TopologicalSpace.IsTopologicalBasis Topology.IsQuotientMap IsOpenMap	Set.image Set	—	TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds isOpen Topology.IsQuotientMap.surjective IsOpen.preimage Topology.IsQuotientMap.continuous exists_subset_of_mem_open HasSubset.Subset.trans Set.instIsTransSubset Set.image_mono Set.image_preimage_subset
mem_closure_iff 📖	mathematical	TopologicalSpace.IsTopologicalBasis	Set Set.instMembership closure Set.Nonempty Set.instInter	—	mem_closure_iff_nhds_basis' nhds_hasBasis
mem_nhds 📖	mathematical	TopologicalSpace.IsTopologicalBasis Set Set.instMembership	Filter Filter.instMembership nhds	—	IsOpen.mem_nhds isOpen
mem_nhds_iff 📖	mathematical	TopologicalSpace.IsTopologicalBasis	Set Filter Filter.instMembership nhds Set.instMembership Set.instHasSubset	—	eq_generateFrom TopologicalSpace.nhds_generateFrom Filter.biInf_sets_eq exists_subset_inter Filter.le_principal_iff HasSubset.Subset.trans Set.instIsTransSubset Set.inter_subset_left Set.inter_subset_right Set.eq_univ_iff_forall sUnion_eq
nhds_hasBasis 📖	mathematical	TopologicalSpace.IsTopologicalBasis	Filter.HasBasis Set nhds Set.instMembership	—	mem_nhds_iff
of_hasBasis_nhds 📖	mathematical	Filter.HasBasis Set nhds Set.instMembership	TopologicalSpace.IsTopologicalBasis	—	Filter.HasBasis.mem_iff Filter.inter_mem Filter.HasBasis.mem_of_mem Set.sUnion_eq_univ_iff Filter.HasBasis.ex_mem TopologicalSpace.ext_nhds TopologicalSpace.nhds_generateFrom iInf_congr_Prop Filter.HasBasis.eq_biInf
of_isOpen_of_subset 📖	—	IsOpen TopologicalSpace.IsTopologicalBasis Set Set.instHasSubset	—	—	TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds isOpen_iff
open_eq_iUnion 📖	mathematical	TopologicalSpace.IsTopologicalBasis IsOpen	Set.iUnion Set Set.instMembership	—	Set.sUnion_eq_iUnion open_eq_sUnion'
open_eq_sUnion 📖	mathematical	TopologicalSpace.IsTopologicalBasis IsOpen	Set Set.instHasSubset Set.sUnion	—	open_eq_sUnion'
open_eq_sUnion' 📖	mathematical	TopologicalSpace.IsTopologicalBasis IsOpen	Set.sUnion setOf Set Set.instMembership Set.instHasSubset	—	Set.ext exists_subset_of_mem_open
open_iff_eq_sUnion 📖	mathematical	TopologicalSpace.IsTopologicalBasis	IsOpen Set Set.instHasSubset Set.sUnion	—	open_eq_sUnion isOpen_sUnion isOpen
prod 📖	mathematical	TopologicalSpace.IsTopologicalBasis	instTopologicalSpaceProd Set.image2 Set SProd.sprod Set.instSProd	—	inf_induced
quotient 📖	mathematical	TopologicalSpace.IsTopologicalBasis IsOpenMap instTopologicalSpaceQuotient	Set.image Set	—	isQuotientMap isQuotientMap_quotient_mk'
sUnion_eq 📖	mathematical	TopologicalSpace.IsTopologicalBasis	Set.sUnion Set.univ	—	—
secondCountableTopology 📖	mathematical	TopologicalSpace.IsTopologicalBasis	SecondCountableTopology	—	eq_generateFrom
sigma 📖	mathematical	TopologicalSpace.IsTopologicalBasis	instTopologicalSpaceSigma Set.iUnion Set Set.image	—	of_hasBasis_nhds Sigma.nhds_eq Set.image_congr Filter.HasBasis.to_image_id Filter.HasBasis.map nhds_hasBasis
subset_of_forall_subset 📖	—	TopologicalSpace.IsTopologicalBasis IsOpen Set Set.instHasSubset	—	—	open_eq_sUnion'
sum 📖	mathematical	TopologicalSpace.IsTopologicalBasis	instTopologicalSpaceSum Set Set.instUnion Set.image	—	TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds Topology.IsOpenEmbedding.isOpenMap Topology.IsOpenEmbedding.inl isOpen Topology.IsOpenEmbedding.inr exists_subset_of_mem_open isOpen_sum_iff Set.mem_union_left Set.mem_image_of_mem Set.image_subset_iff Set.mem_union_right

TopologicalSpace.Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
secondCountableTopology 📖	mathematical	IsOpenMap instTopologicalSpaceQuotient	SecondCountableTopology	—	Topology.IsQuotientMap.secondCountableTopology isQuotientMap_quotient_mk'

TopologicalSpace.SecondCountableTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk' 📖	mathematical	—	SecondCountableTopology TopologicalSpace.generateFrom	—	—
to_firstCountableTopology 📖	mathematical	—	FirstCountableTopology	—	Filter.HasCountableBasis.isCountablyGenerated TopologicalSpace.IsTopologicalBasis.nhds_hasBasis TopologicalSpace.isBasis_countableBasis Set.Countable.mono Set.inter_subset_left TopologicalSpace.countable_countableBasis
to_separableSpace 📖	mathematical	—	TopologicalSpace.SeparableSpace	—	Set.countable_range Encodable.countable TopologicalSpace.IsTopologicalBasis.dense_iff TopologicalSpace.isBasis_countableBasis Set.mem_range_self TopologicalSpace.nonempty_of_mem_countableBasis

TopologicalSpace.SeparableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_countable_dense 📖	mathematical	—	Set.Countable Dense	—	—
of_denseRange 📖	mathematical	DenseRange	TopologicalSpace.SeparableSpace	—	Set.countable_range

TopologicalSpace.Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
firstCountableTopology 📖	mathematical	—	FirstCountableTopology Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	TopologicalSpace.firstCountableTopology_induced
secondCountableTopology 📖	mathematical	—	SecondCountableTopology Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	TopologicalSpace.secondCountableTopology_induced

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
firstCountableTopology 📖	mathematical	Topology.IsEmbedding	FirstCountableTopology	—	Topology.IsInducing.firstCountableTopology toIsInducing
secondCountableTopology 📖	mathematical	Topology.IsEmbedding	SecondCountableTopology	—	Topology.IsInducing.secondCountableTopology toIsInducing
separableSpace 📖	mathematical	Topology.IsEmbedding	TopologicalSpace.SeparableSpace	—	secondCountableTopology TopologicalSpace.SecondCountableTopology.to_separableSpace

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
firstCountableTopology 📖	mathematical	Topology.IsInducing	FirstCountableTopology	—	eq_induced TopologicalSpace.firstCountableTopology_induced
secondCountableTopology 📖	mathematical	Topology.IsInducing	SecondCountableTopology	—	eq_induced TopologicalSpace.secondCountableTopology_induced

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
separableSpace 📖	mathematical	Topology.IsOpenEmbedding	TopologicalSpace.SeparableSpace	—	IsOpenMap.separableSpace_of_injective isOpenMap Topology.IsEmbedding.injective toIsEmbedding

Topology.IsQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
secondCountableTopology 📖	mathematical	Topology.IsQuotientMap IsOpenMap	SecondCountableTopology	—	TopologicalSpace.exists_countable_basis Set.Countable.image TopologicalSpace.IsTopologicalBasis.eq_generateFrom TopologicalSpace.IsTopologicalBasis.isQuotientMap
separableSpace 📖	mathematical	Topology.IsQuotientMap	TopologicalSpace.SeparableSpace	—	DenseRange.separableSpace Function.Surjective.denseRange surjective continuous

(root)

Definitions

Name	Category	Theorems
FirstCountableTopology 📖	CompData	18 math math: WithSeminorms.firstCountableTopology, TopologicalSpace.instFirstCountableTopologyProd, instFirstCountableTopologyOrderDual, TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology, DiscreteTopology.firstCountableTopology, Rat.not_firstCountableTopology_opc, SchwartzMap.instFirstCountableTopology, AlexandrovDiscrete.toFirstCountable, QuotientAddGroup.instFirstCountableTopology, TopologicalSpace.SecondCountableTopology.to_firstCountableTopology, UniformSpace.firstCountableTopology, Topology.IsInducing.firstCountableTopology, QuotientGroup.instFirstCountableTopology, TopologicalSpace.Subtype.firstCountableTopology, Topology.IsEmbedding.firstCountableTopology, DomAddAct.instFirstCountableTopology, DomMulAct.instFirstCountableTopology, TopologicalSpace.firstCountableTopology_induced
SecondCountableTopology 📖	CompData	168 math math: DomAddAct.instSecondCountableTopology, LightCondensed.free_internallyProjective_iff_tensor_condition, LightProfinite.proj_comp_transitionMap, LightProfinite.Extend.functorOp_obj, LightCondensed.lanPresheafIso_hom, LightCondensed.isoFinYonedaComponents_hom_apply, Topology.IsEmbedding.secondCountableTopology, LightCondensed.ihomPoints_apply, TopologicalSpace.SecondCountableTopology.mk', LightCondensed.forget_obj_val_map, QuotientGroup.instSecondCountableTopology, SecondCountableTopology.of_separableSpace_orderTopology, Metric.Snowflaking.instSecondCountableTopology, LightCondensed.ihomPoints_symm_comp, instSecondCountableTopologyOfOrderTopologyOfCountable, LightCondSet.continuous_coinducingCoprod, LightCondSet.epi_iff_locallySurjective_on_lightProfinite, LightProfinite.instCountableClopensCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, LightCondensed.isoFinYoneda_inv_app, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition, ModelWithCorners.secondCountableTopology, NNReal.instSecondCountableTopology, instFaithfulFintypeCatLightProfiniteToLightProfinite, LightCondensed.finYoneda_map, TopologicalSpace.instSecondCountableTopologyWithTop, LightCondMod.isDiscrete_tfae, QuotientAddGroup.instSecondCountableTopology, instPreservesEpimorphismsLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightProfinite.instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace, LightCondensed.discrete_map, LightProfinite.proj_comp_transitionMapLE', LightProfinite.Extend.cocone_ι_app, Profinite.injective_of_light, LightCondSet.topCatAdjunctionUnit_val_app_apply, ContinuousConstSMul.secondCountableTopology, lightProfiniteToLightDiagram_map, LightProfinite.isClosedMap, TopologicalSpace.Subtype.secondCountableTopology, lightDiagramToLightProfinite_obj, LightProfinite.lightToProfinite_map_proj_eq, Homeomorph.secondCountableTopology, TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace, LightProfinite.effectiveEpi_iff_surjective, MeasureTheory.Lp.SecondCountableTopology, LightProfinite.continuous_iff_convergent, LightCondensed.internallyProjective_iff_tensor_condition, TopologicalSpace.Opens.instSecondCountableOpens, DiscreteTopology.secondCountableTopology_of_countable, LightProfinite.instPreservesEpimorphismsProfiniteLightToProfinite, LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology, LightProfinite.instCountableDiscreteQuotient, instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightProfinite.hasSheafify, LightCondMod.LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, LightProfinite.instWEqualsLocallyBijectiveCoherentTopology, TopologicalSpace.Quotient.secondCountableTopology, TopologicalSpace.IsSeparable.secondCountableTopology, LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, TopologicalSpace.instSecondCountableTopologySum, DomMulAct.instSecondCountableTopology, instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory, LightCondensed.isoFinYonedaComponents_inv_comp, ChartedSpace.secondCountable_of_sigmaCompact, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition', ContinuousConstVAdd.secondCountableTopology, instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightProfinite.Extend.functor_map, LightCondensed.instPreservesLimitsOfShapeOppositeLightProfiniteDiscreteCarrier, EReal.instSecondCountableTopology, Topology.IsQuotientMap.secondCountableTopology, LightCondensed.forget_map_val_app, LightCondensed.isoLocallyConstantOfIsColimit_inv, FintypeCat.toLightProfinite_map_hom_hom_apply, Topology.IsInducing.secondCountableTopology, LightProfinite.injective, LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite, LightProfinite.surjective_transitionMapLE, exists_opensMeasurableSpace_of_countablySeparated, LightProfinite.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopology, LightCondensed.free_internallyProjective_iff_tensor_condition', LightProfinite.instHasCountableLimits, LightProfinite.forget_reflectsIsomorphisms, LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology, UniformSpace.secondCountable_of_separable, instIsEquivalenceLightDiagramLightProfiniteLightDiagramToLightProfinite, EMetric.secondCountable_of_sigmaCompact, TopologicalSpace.secondCountableTopology_induced, LightProfinite.Extend.functorOp_map, LightProfinite.instTotallyDisconnectedSpaceCarrierToTopAndSecondCountableTopology, instEssentiallySmallLightProfinite, LightCondensed.hom_ext_iff, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, TopologicalSpace.instSecondCountableTopologyOfCountableOfFirstCountableTopology, LightCondensed.underlying_obj, OpenPartialHomeomorph.secondCountableTopology_source, Rat.not_secondCountableTopology_opc, LightCondSet.hom_naturality_apply, LightProfinite.instTotallyDisconnectedSpaceCarrierToTopTruePtCompHausLimitConeCompLightProfiniteToCompHaus, LightProfinite.instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, LightCondensed.equalizerCondition, LightCondMod.hom_naturality_apply, LightCondensed.ihomPoints_symm_apply, LightCondensed.discrete_obj, ContinuousMap.instSecondCountableTopology, lightProfiniteToLightDiagram_obj, LightCondMod.LocallyConstant.instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, LightCondensed.lanPresheafNatIso_hom_app, lightCondSetToTopCat_obj_carrier, GromovHausdorff.instSecondCountableTopologyGHSpace, ContinuousMap.secondCountableTopology, LightProfinite.Extend.cocone_pt, LightCondMod.epi_iff_locallySurjective_on_lightProfinite, LightCondensed.ihom_map_val_app, instSecondCountableTopologyContinuousLinearMapIdOfFiniteDimensional, LightCondSet.LocallyConstant.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopologySubtypeToTop, UniformSpace.secondCountable_of_almost_dense_set, EMetric.secondCountable_of_almost_dense_set, instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet, lightDiagramToLightProfinite_map, LightProfinite.surjective_transitionMap, Metric.secondCountable_of_countable_discretization, SecondCountableTopologyEither.out, UpperHalfPlane.instSecondCountableTopology, Metric.secondCountable_of_almost_dense_set, LightCondensed.lanPresheafExt_inv, LightProfinite.epi_iff_surjective, TopologicalSpace.Clopens.countable_iff_secondCountable, instSecondCountableTopologyReal, LightCondMod.LocallyConstant.instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf, LightCondSet.isDiscrete_tfae, LightCondSet.topCatAdjunctionUnit_val_app, LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp, LightProfinite.instPreregular, LightCondMod.LocallyConstant.instHasSheafifyLightProfiniteCoherentTopologyModuleCat, LightCondensed.id_val, LightProfinite.Extend.functor_obj, LightCondensed.isoFinYoneda_hom_app, ENNReal.instSecondCountableTopology, LightProfinite.proj_surjective, PolishSpace.toSecondCountableTopology, LightProfinite.proj_comp_transitionMapLE, LightProfinite.instEpiAppOppositeNatπAsLimitCone, LightCondMod.LocallyConstant.instFaithfulSheafLightProfiniteCoherentTopologyTypeConstantSheaf, LightCondensed.instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType, instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone, LightCondensed.internallyProjective_iff_tensor_condition', LightProfinite.hasSheafify_type, LightCondensed.comp_val, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_app_hom_hom, ChartedSpace.secondCountable_of_countable_cover, LightCondensed.underlying_map, TopologicalSpace.Opens.CompleteCopy.instSecondCountableTopology, LightCondMod.isDiscrete_iff_isDiscrete_forget, instIsEquivalenceLightProfiniteLightDiagramLightProfiniteToLightDiagram, LightCondSet.toTopCatMap_hom_apply, LightCondensed.lanPresheafExt_hom, exists_borelSpace_of_countablyGenerated_of_separatesPoints, LightProfinite.proj_comp_transitionMap', instFullFintypeCatLightProfiniteToLightProfinite, secondCountable_of_proper, TopologicalSpace.IsTopologicalBasis.secondCountableTopology, Finite.toSecondCountableTopology, instSecondCountableTopologyOrderDual, WithLp.secondCountableTopology, LightCondensed.instPreservesFiniteProductsOppositeLightProfiniteVal, TopologicalSpace.instSecondCountableTopologyProd, LightCondensed.instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology, TopologicalSpace.NonemptyCompacts.instSecondCountableTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_countable_dense_bot_top 📖	mathematical	—	Set.Countable Dense Set Set.instMembership	—	Dense.exists_countable_dense_subset_bot_top separableSpace_univ dense_univ
isOpenMap_eval 📖	mathematical	—	IsOpenMap Pi.topologicalSpace Function.eval	—	TopologicalSpace.IsTopologicalBasis.isOpenMap_iff isTopologicalBasis_pi TopologicalSpace.isTopologicalBasis_opens Set.eq_empty_or_nonempty Set.image_congr Set.image_empty Set.eval_image_pi Set.eval_image_pi_of_notMem isOpen_univ
isTopologicalBasis_pi 📖	mathematical	TopologicalSpace.IsTopologicalBasis	Pi.topologicalSpace setOf Set Finset Set.pi SetLike.coe Finset.instSetLike	—	Set.pi_def IsTopologicalBasis.iInf_induced
isTopologicalBasis_singletons 📖	mathematical	—	TopologicalSpace.IsTopologicalBasis setOf Set Set.instSingletonSet	—	TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds isOpen_discrete Set.mem_singleton Set.singleton_subset_iff
isTopologicalBasis_subtype 📖	mathematical	TopologicalSpace.IsTopologicalBasis	instTopologicalSpaceSubtype Set.image Set Set.preimage	—	TopologicalSpace.IsTopologicalBasis.isInducing
separableSpace_univ 📖	mathematical	—	TopologicalSpace.SeparableSpace Set.Elem Set.univ instTopologicalSpaceSubtype Set Set.instMembership	—	DenseRange.separableSpace Function.Surjective.denseRange Equiv.surjective continuous_id

---

← Back to Index