Basic

📁 Source: Mathlib/Topology/Separation/Basic.lean

Statistics

Metric	Count
Definitions relativelyCompact, R0Space, R1Space, T0Space, T1Space, specializationOrder	6
Theorems isBounded_iff, relativelyCompact_eq_inCompact, continuous_of, eq_const_of_mem_closure, isOpen_mulSupport, isOpen_support, eventually_ne, eqOn_const_closure, eq_const_of_mem_closure, insert', of_insert, diff_finite, diff_finset, diff_singleton, exists_inter_eq_singleton_of_mem_discrete, eventually_ne, coclosedCompact_eq_cocompact, coclosedCompact_le_cofinite, instDiscreteTopology, isClosed, update_eventuallyEq_nhdsNE, t0Space, t1Space, eq, of_nhds_neBot, exists_closed_singleton, binary_compact_cover, closure, closure_eq_biUnion_closure_singleton, closure_eq_biUnion_inseparable, closure_of_subset, closure_subset_of_isOpen, finite_compact_cover, isCompact_isClosed_basis_nhds, mem_closure_iff_exists_inseparable, nhdsWithin_compl_singleton, nhdsWithin_diff_singleton, instT0Space, instT0Space, closure_singleton, specializes_symmetric, iInf, induced, inf, of_continuous_specializes_imp, sInf, specializes_or_disjoint_nhds, of_isCompact_isCompact_isClosed, instT0Space, t1Space_iff, continuousOn, isClosed, isCompact_closure, isDiscrete, closure, closure_eq, isClosed, eq, inseparable, t0Space, t1Space, of_cover, of_open_cover, t0, t0Space, t1, eq_iff, exists_mem_of_ne, inseparable_iff, t0Space, t1Space, injective, isEmbedding, r0Space, r1Space, instT0Space, instT1Space, locallyCompactSpace, biInter_basis_nhds, closure_singleton, compl_singleton_mem_nhds, compl_singleton_mem_nhdsSet_iff, compl_singleton_mem_nhds_iff, continuousAt_of_tendsto_nhds, continuousAt_update_of_ne, continuousOn_update_iff, continuousWithinAt_congr_set', continuousWithinAt_diff_singleton, continuousWithinAt_insert, continuousWithinAt_update_of_ne, disjoint_nhdsWithin_of_mem_discrete, disjoint_nhds_nhds_iff_not_inseparable, disjoint_nhds_nhds_iff_not_specializes, disjoint_nhds_pure, disjoint_pure_nhds, eq_of_tendsto_nhds, eventuallyEq_insert, eventually_ne_nhds, eventually_ne_nhdsWithin, eventually_nhdsNE_eventually_nhds_iff, eventually_nhdsWithin_eventually_nhds_iff_of_isOpen, exists_isCompact_superset_iff, exists_isOpen_mem_isCompact_closure, exists_isOpen_singleton_of_isOpen_finite, exists_isOpen_superset_and_isCompact_closure, exists_isOpen_xor'_mem, exists_mem_nhds_isCompact_isClosed, exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds, exists_open_singleton_of_finite, infinite_of_mem_nhds, injective_nhdsSet, inseparable_eq_eq, inseparable_iff_eq, insert_mem_nhdsWithin_of_subset_insert, instLocallyCompactPairOfWeaklyLocallyCompactSpaceOfR1Space, instR0Space, instR0SpaceForall, instR0SpaceOfT1Space, instR0SpaceProd, instR0SpaceSubtype, instR1SpaceForall, instR1SpaceProd, instR1SpaceSubtype, instT1SpaceCofiniteTopology, instT1SpaceForall, instT1SpaceOfDiscreteTopology, instT1SpaceOfT0SpaceOfR0Space, instT1SpaceProd, isClosedEmbedding_update, isClosedMap_const, isClosedMap_prodMk_left, isClosedMap_prodMk_right, isClosed_inter_singleton, isClosed_setOf_inseparable, isClosed_setOf_specializes, isClosed_singleton, isClosed_singleton_inter, isCompact_closure_singleton, isCompact_isClosed_basis_nhds, isEmbedding_iff_isInducing, isOpen_compl_singleton, isOpen_inter_eq_singleton_of_mem_discrete, isOpen_ne, isOpen_setOf_eventually_nhdsWithin, isOpen_singleton_of_finite_mem_nhds, ker_nhds, minimal_nonempty_closed_eq_singleton, minimal_nonempty_closed_subsingleton, minimal_nonempty_open_eq_singleton, minimal_nonempty_open_subsingleton, nhdsNE_le_cofinite, nhdsSet_inj_iff, nhdsSet_le_iff, nhdsWithin_compl_singleton_le, nhdsWithin_insert_of_ne, nhdsWithin_of_mem_discrete, nhds_eq_nhds_iff, nhds_injective, nhds_inter_eq_singleton_of_mem_discrete, nhds_le_nhdsSet_iff, nhds_le_nhds_iff, pure_le_nhds_iff, r0Space_iff, r1Space_iff_inseparable_or_disjoint_nhds, r1Space_iff_specializes_or_disjoint_nhds, r1_separation, singleton_mem_nhdsWithin_of_mem_discrete, specializes_comm, specializes_eq_eq, specializes_iff_eq, specializes_iff_inseparable, specializes_iff_not_disjoint, strictMono_nhdsSet, subsingleton_closure, t0Space_iff_exists_isOpen_xor'_mem, t0Space_iff_inseparable, t0Space_iff_nhds_injective, t0Space_iff_not_inseparable, t0Space_iff_or_notMem_closure, t0Space_of_injective_of_continuous, t1Space_TFAE, t1Space_antitone, t1Space_iff_continuous_cofinite_of, t1Space_iff_disjoint_nhds_pure, t1Space_iff_disjoint_pure_nhds, t1Space_iff_exists_open, t1Space_iff_specializes_imp_eq, t1Space_iff_t0Space_and_r0Space, t1Space_of_injective_of_continuous, tendsto_const_nhds_iff, tendsto_nhds_unique_inseparable	191
Total	197

Bornology

Definitions

Name	Category	Theorems
relativelyCompact 📖	CompOp	2 math math: relativelyCompact.isBounded_iff, relativelyCompact_eq_inCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
relativelyCompact_eq_inCompact 📖	mathematical	—	relativelyCompact instR0Space inCompact	—	ext instR0Space Filter.coclosedCompact_eq_cocompact

Bornology.relativelyCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBounded_iff 📖	mathematical	—	Bornology.IsBounded Bornology.relativelyCompact IsCompact closure	—	Filter.compl_mem_coclosedCompact

CofiniteTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_of 📖	mathematical	—	Continuous CofiniteTopology instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike of	—	t1Space_iff_continuous_cofinite_of

ContinousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_const_of_mem_closure 📖	—	ContinuousWithinAt Set Set.instMembership closure	—	—	ContinuousWithinAt.eq_const_of_mem_closure

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpen_mulSupport 📖	mathematical	Continuous	IsOpen Function.mulSupport	—	IsOpen.preimage isOpen_ne
isOpen_support 📖	mathematical	Continuous	IsOpen Function.support	—	IsOpen.preimage isOpen_ne

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_ne 📖	mathematical	ContinuousAt	Filter.Eventually nhds	—	Filter.Tendsto.eventually_ne tendsto

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqOn_const_closure 📖	mathematical	ContinuousWithinAt Set.EqOn	closure	—	eq_const_of_mem_closure
eq_const_of_mem_closure 📖	—	ContinuousWithinAt Set Set.instMembership closure	—	—	Set.mem_singleton_iff closure_singleton mem_closure
insert' 📖	mathematical	ContinuousWithinAt	Set Set.instInsert	—	continuousWithinAt_insert
of_insert 📖	—	ContinuousWithinAt Set Set.instInsert	—	—	continuousWithinAt_insert

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
diff_finite 📖	mathematical	Filter.NeBot nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet Dense	Set.instSDiff	—	Set.Finite.coe_toFinset diff_finset
diff_finset 📖	mathematical	Filter.NeBot nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet Dense	Set.instSDiff SetLike.coe Finset Finset.instSetLike	—	Finset.induction_on Finset.coe_empty Set.diff_empty Finset.coe_insert Set.union_singleton Set.diff_diff diff_singleton
diff_singleton 📖	mathematical	Dense	Set Set.instSDiff Set.instSingletonSet	—	inter_of_isOpen_right dense_compl_singleton isOpen_compl_singleton

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coclosedCompact_eq_cocompact 📖	mathematical	—	coclosedCompact cocompact	—	le_antisymm HasBasis.le_basis_iff hasBasis_coclosedCompact hasBasis_cocompact isClosed_closure IsCompact.closure Set.compl_subset_compl subset_closure cocompact_le_coclosedCompact
coclosedCompact_le_cofinite 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder coclosedCompact cofinite	—	le_cofinite_iff_compl_singleton_mem compl_mem_coclosedCompact isCompact_closure_singleton

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_inter_eq_singleton_of_mem_discrete 📖	mathematical	IsDiscrete Filter.HasBasis nhds Set Set.instMembership	Set.instInter Set.instSingletonSet	—	mem_iff nhdsWithin_hasBasis singleton_mem_nhdsWithin_of_mem_discrete HasSubset.Subset.antisymm Set.instAntisymmSubset Set.singleton_subset_iff mem_of_mem_nhds mem_of_mem

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_ne 📖	mathematical	Filter.Tendsto nhds	Filter.Eventually	—	eventually IsOpen.eventually_mem isOpen_compl_singleton

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDiscreteTopology 📖	mathematical	—	DiscreteTopology	—	discreteTopology_iff_forall_isClosed Set.Finite.isClosed Set.toFinite Subtype.finite

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed 📖	mathematical	—	IsClosed SetLike.coe Finset instSetLike	—	Set.Finite.isClosed finite_toSet

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
update_eventuallyEq_nhdsNE 📖	mathematical	—	Filter.EventuallyEq nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet update	—	Filter.EventuallyEq.filter_mono update_eventuallyEq_cofinite nhdsNE_le_cofinite

Homeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
t0Space 📖	mathematical	—	T0Space	—	Topology.IsEmbedding.t0Space isEmbedding
t1Space 📖	mathematical	—	T1Space	—	Topology.IsEmbedding.t1Space isEmbedding

Inseparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq 📖	—	Inseparable	—	—	T0Space.t0
of_nhds_neBot 📖	mathematical	—	Inseparable	—	r1Space_iff_inseparable_or_disjoint_nhds Filter.NeBot.ne Disjoint.eq_bot

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_closed_singleton 📖	mathematical	Set.Nonempty	Set Set.instMembership IsClosed Set.instSingletonSet	—	exists_minimal_nonempty_closed_subset minimal_nonempty_closed_eq_singleton Set.mem_singleton

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
binary_compact_cover 📖	—	IsCompact IsOpen Set Set.instHasSubset Set.instUnion	—	—	closure SeparatedNhds.of_isCompact_isCompact_isClosed diff IsClosed.sdiff isClosed_closure Set.disjoint_iff_inter_eq_empty Set.diff_inter_diff Set.diff_eq_empty closure_subset_of_isOpen IsOpen.union SeparatedNhds.mono Set.diff_subset_diff_left subset_closure Set.diff_subset_comm Set.diff_inter Disjoint.inter_eq Set.diff_empty
closure 📖	mathematical	IsCompact	closure	—	isCompact_of_finite_subcover elim_finite_subcover HasSubset.Subset.trans Set.instIsTransSubset subset_closure closure_subset_of_isOpen isOpen_biUnion
closure_eq_biUnion_closure_singleton 📖	mathematical	IsCompact	closure Set.iUnion Set Set.instMembership Set.instSingletonSet	—	closure_eq_biUnion_inseparable Set.iUnion_congr_Prop instR0Space
closure_eq_biUnion_inseparable 📖	mathematical	IsCompact	closure Set.iUnion Set Set.instMembership setOf Inseparable	—	Set.ext mem_closure_iff_exists_inseparable
closure_of_subset 📖	mathematical	IsCompact Set Set.instHasSubset	closure	—	of_isClosed_subset closure isClosed_closure closure_mono
closure_subset_of_isOpen 📖	mathematical	IsCompact IsOpen Set Set.instHasSubset	closure	—	closure_eq_biUnion_inseparable Set.iUnion₂_subset_iff Inseparable.mem_open_iff
finite_compact_cover 📖	—	IsCompact IsOpen Set Set.instHasSubset Set.iUnion Finset Finset.instMembership	—	—	Finset.induction isCompact_empty Set.empty_subset Set.iUnion_congr_Prop Set.iUnion_empty Set.iUnion_false binary_compact_cover isOpen_biUnion Finset.set_biUnion_insert eq_or_ne Function.update_self Function.update_of_ne Finset.set_biUnion_insert_update
isCompact_isClosed_basis_nhds 📖	mathematical	IsCompact Set Filter Filter.instMembership nhds	Filter.HasBasis IsClosed	—	Filter.hasBasis_self exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds continuous_id interior_mem_nhds Filter.mem_of_superset subset_closure closure isClosed_closure HasSubset.Subset.trans Set.instIsTransSubset closure_subset_of_isOpen isOpen_interior interior_subset
mem_closure_iff_exists_inseparable 📖	mathematical	IsCompact	Set Set.instMembership closure Inseparable	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq disjoint_nhdsSet_right Disjoint.symm disjoint_nhds_nhds_iff_not_inseparable Disjoint.mono_right principal_le_nhdsSet Inseparable.mem_closed_iff isClosed_closure subset_closure

Ne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nhdsWithin_compl_singleton 📖	mathematical	—	nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet nhds	—	IsOpen.nhdsWithin_eq isOpen_ne
nhdsWithin_diff_singleton 📖	mathematical	—	nhdsWithin Set Set.instSDiff Set.instSingletonSet	—	Set.diff_eq Set.inter_comm nhdsWithin_inter_of_mem mem_nhdsWithin_of_mem_nhds IsOpen.mem_nhds isOpen_ne

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instT0Space 📖	mathematical	T0Space	topologicalSpace	—	Inseparable.eq Inseparable.map continuous_apply

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instT0Space 📖	mathematical	—	T0Space instTopologicalSpaceProd	—	Inseparable.eq Inseparable.map continuous_fst continuous_snd

R0Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_singleton 📖	mathematical	—	closure Set Set.instSingletonSet Filter.ker nhds	—	Set.ext ker_nhds_eq_specializes
specializes_symmetric 📖	mathematical	—	Symmetric Specializes	—	—

R1Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iInf 📖	mathematical	R1Space	iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	sInf Set.forall_mem_range
induced 📖	mathematical	—	R1Space TopologicalSpace.induced	—	Topology.IsInducing.r1Space Topology.IsInducing.induced
inf 📖	mathematical	—	R1Space TopologicalSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	inf_eq_iInf iInf
of_continuous_specializes_imp 📖	mathematical	Continuous Specializes	R1Space	—	Filter.Tendsto.disjoint Continuous.tendsto specializes_or_disjoint_nhds
sInf 📖	mathematical	R1Space	InfSet.sInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	nhds_sInf Disjoint.mono iInf₂_le iInf₂_mono specializes_or_disjoint_nhds Mathlib.Tactic.Push.not_and_eq
specializes_or_disjoint_nhds 📖	mathematical	—	Specializes Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhds	—	—

SeparatedNhds

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isCompact_isCompact_isClosed 📖	mathematical	IsCompact Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	SeparatedNhds	—	IsCompact.disjoint_nhdsSet_left IsCompact.disjoint_nhdsSet_right Inseparable.mem_closed_iff Set.disjoint_left

SeparationQuotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instT0Space 📖	mathematical	—	T0Space SeparationQuotient instTopologicalSpaceSeparationQuotient	—	Quotient.inductionOn₂' Topology.IsInducing.inseparable_iff
t1Space_iff 📖	mathematical	—	T1Space SeparationQuotient instTopologicalSpaceSeparationQuotient R0Space	—	r0Space_iff List.TFAE.out t1Space_TFAE Topology.IsInducing.specializes_iff specializes_refl inseparable_iff_specializes_and

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn 📖	mathematical	—	ContinuousOn	—	continuousOn_iff_continuous_restrict continuous_of_discreteTopology Finite.instDiscreteTopology Subtype.t1Space
isClosed 📖	mathematical	—	IsClosed	—	Set.biUnion_of_singleton isClosed_biUnion isClosed_singleton
isCompact_closure 📖	mathematical	—	IsCompact closure	—	Bornology.relativelyCompact.isBounded_iff isBounded
isDiscrete 📖	mathematical	—	IsDiscrete	—	Finite.instDiscreteTopology Subtype.t1Space to_subtype

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	mathematical	Set.Subsingleton	closure	—	closure_eq
closure_eq 📖	mathematical	Set.Subsingleton	closure	—	IsClosed.closure_eq isClosed
isClosed 📖	mathematical	Set.Subsingleton	IsClosed	—	eq_empty_or_singleton isClosed_empty isClosed_singleton

Specializes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq 📖	—	Specializes	—	—	t1Space_iff_specializes_imp_eq
inseparable 📖	mathematical	Specializes	Inseparable	—	specializes_iff_inseparable

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
t0Space 📖	mathematical	—	T0Space instTopologicalSpaceSubtype	—	Topology.IsEmbedding.t0Space Topology.IsEmbedding.subtypeVal
t1Space 📖	mathematical	—	T1Space instTopologicalSpaceSubtype	—	Topology.IsEmbedding.t1Space Topology.IsEmbedding.subtypeVal

T0Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_cover 📖	—	Set Set.instMembership T0Space Set.Elem instTopologicalSpaceSubtype	—	—	CanLift.prf Subtype.canLift Inseparable.eq subtype_inseparable_iff
of_open_cover 📖	—	Set Set.instMembership IsOpen T0Space Set.Elem instTopologicalSpaceSubtype	—	—	of_cover Inseparable.mem_open_iff
t0 📖	—	Inseparable	—	—	—

T1Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
t0Space 📖	mathematical	—	T0Space	—	t1Space_iff_t0Space_and_r0Space
t1 📖	mathematical	—	IsClosed Set Set.instSingletonSet	—	—

TopologicalSpace.IsTopologicalBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_iff 📖	mathematical	TopologicalSpace.IsTopologicalBasis	Set Set.instMembership	—	inseparable_iff_eq inseparable_iff
exists_mem_of_ne 📖	mathematical	TopologicalSpace.IsTopologicalBasis	Set Set.instMembership	—	isOpen_iff isOpen_ne
inseparable_iff 📖	mathematical	TopologicalSpace.IsTopologicalBasis	Inseparable Set Set.instMembership	—	inseparable_iff_forall_isOpen isOpen Filter.HasBasis.eq_of_same_basis nhds_hasBasis

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
t0Space 📖	mathematical	Topology.IsEmbedding	T0Space	—	t0Space_of_injective_of_continuous injective continuous
t1Space 📖	mathematical	Topology.IsEmbedding	T1Space	—	t1Space_of_injective_of_continuous injective continuous

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective 📖	—	Topology.IsInducing	—	—	Inseparable.eq inseparable_iff Inseparable.of_eq
isEmbedding 📖	mathematical	Topology.IsInducing	Topology.IsEmbedding	—	injective
r0Space 📖	mathematical	Topology.IsInducing	R0Space	—	specializes_iff Specializes.symm
r1Space 📖	mathematical	Topology.IsInducing	R1Space	—	R1Space.of_continuous_specializes_imp continuous specializes_iff

ULift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instT0Space 📖	mathematical	—	T0Space topologicalSpace	—	Topology.IsEmbedding.t0Space Topology.IsEmbedding.uliftDown
instT1Space 📖	mathematical	—	T1Space topologicalSpace	—	Topology.IsEmbedding.t1Space Topology.IsEmbedding.uliftDown

WeaklyLocallyCompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallyCompactSpace 📖	mathematical	—	LocallyCompactSpace	—	LocallyCompactSpace.of_hasBasis isCompact_isClosed_basis_nhds

(root)

Definitions

Name	Category	Theorems
R0Space 📖	CompData	14 math math: instR0SpaceOfT1Space, SeparationQuotient.t1Space_iff, t1Space_TFAE, Topology.IsInducing.r0Space, ContinuousMapZero.instR0Space, DomAddAct.instR0Space, instR0SpaceOfPerfectlyNormalSpace, instR0SpaceSubtype, r0Space_iff, instR0SpaceProd, instR0Space, ContinuousMap.instR0Space, t1Space_iff_t0Space_and_r0Space, DomMulAct.instR0Space
R1Space 📖	CompData	17 math math: instR1SpaceProd, R1Space.of_continuous_specializes_imp, MeasureTheory.FiniteMeasure.instR1Space, Topology.IsInducing.r1Space, r1Space_iff_inseparable_or_disjoint_nhds, R1Space.induced, R1Space.inf, DomAddAct.instR1Space, instR1SpaceSubtype, T2Space.r1Space, r1Space_iff_specializes_or_disjoint_nhds, SeparationQuotient.t2Space_iff, ContinuousMapZero.instR1Space, DomMulAct.instR1Space, ContinuousMap.instR1Space, instR1Space, MeasureTheory.ProbabilityMeasure.R1Space
T0Space 📖	CompData	52 math math: T35Space.toT0Space, Topology.IsScott.instT0Space, Topology.IsEmbedding.t0Space, t0Space_iff_inseparable, WithLp.instProdT0Space, SpectralSpace.toT0Space, PrimeSpectrum.instT0Space, t0Space_of_injective_of_continuous, SeparationQuotient.instT0Space, t0Space_iff_uniformity, t0Space_iff_nhds_injective, T3Space.toT0Space, t0Space_iff_uniformity', R1Space.t2Space_iff_t0Space, RegularSpace.t3Space_iff_t0Space, Homeomorph.t0Space, CpltSepUniformSpace.isT0, ContinuousMapZero.instT0Space, AlgebraicGeometry.instT0SpaceCarrierCarrierCommRingCat, CpltSepUniformSpace.t0Space, AbstractCompletion.separation, ValuedRing.separated, t1Space_TFAE, CompletableTopField.toT0Space, DomAddAct.instT0Space, Matrix.instT0Space, Prod.instT0Space, OnePoint.instT0Space, MetricSpace.instT0Space, t0Space_iff_exists_isOpen_xor'_mem, TopologicalSpace.MetrizableSpace.toT0Space, t0Space_iff_ker_uniformity, TopologicalSpace.Opens.CompleteCopy.instT0Space, T1Space.t0Space, T6Space.toT0Space, UniformSpace.Completion.t0Space, t0Space_iff_not_inseparable, t35Space_iff, Topology.IsUpper.t0Space, ULift.instT0Space, EMetricSpace.instT0Space, Filter.instT0Space, t0Space_iff_or_notMem_closure, Metric.Snowflaking.instT0Space, MvPowerSeries.WithPiTopology.instT0Space, Subtype.t0Space, PowerSeries.WithPiTopology.instT0Space, DomMulAct.instT0Space, ContinuousMap.instT0Space, t1Space_iff_t0Space_and_r0Space, TopologicalSpace.Closeds.instT0Space, Topology.IsLower.t0Space
T1Space 📖	CompData	44 math math: t1Space_iff_specializes_imp_eq, WithSeminorms.separating_iff_T1, instT1SpaceCofiniteTopology, MaximalSpectrum.instT1Space, t1Space_iff_disjoint_nhds_pure, IsTopologicalGroup.t1Space, t1Space_iff_exists_open, AddAction.IsPretransitive.t1Space_iff, PrimeSpectrum.t1Space_iff_isField, ContinuousMap.instT1Space, T5Space.toT1Space, IsTopologicalAddGroup.t1Space, WithSeminorms.T1_of_separating, Topology.IsLawson.toT1Space, QuotientAddGroup.t1Space_iff, t1Space_antitone, SeparationQuotient.t1Space_iff, instT1SpaceOfT0SpaceOfR0Space, t1Space_TFAE, ContinuousMapZero.instT1Space, Continuous.homeoOfEquivCompactToT2.t1_counterexample, SeparatingDual.t1Space, Topology.IsEmbedding.t1Space, t1Space_iff_disjoint_pure_nhds, Subtype.t1Space, T2Space.t1Space, t1Space_iff_continuous_cofinite_of, DomMulAct.instT1Space, DomAddAct.instT1Space, t1Space_of_injective_of_continuous, ModelWithCorners.t1Space, ChartedSpace.t1Space, Homeomorph.t1Space, T4Space.toT1Space, QuotientGroup.instT1Space, instT1SpaceOfDiscreteTopology, QuotientAddGroup.instT1Space, OnePoint.instT1Space, t1Space_iff_t0Space_and_r0Space, TotallyDisconnectedSpace.t1Space, MulAction.IsPretransitive.t1Space_iff, instT1SpaceProd, QuotientGroup.t1Space_iff, ULift.instT1Space
specializationOrder 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biInter_basis_nhds 📖	mathematical	Filter.HasBasis nhds	Set.iInter Set Set.instSingletonSet	—	Filter.HasBasis.ker ker_nhds
closure_singleton 📖	mathematical	—	closure Set Set.instSingletonSet	—	IsClosed.closure_eq isClosed_singleton
compl_singleton_mem_nhds 📖	mathematical	—	Set Filter Filter.instMembership nhds Compl.compl Set.instCompl Set.instSingletonSet	—	compl_singleton_mem_nhds_iff
compl_singleton_mem_nhdsSet_iff 📖	mathematical	—	Set Filter Filter.instMembership nhdsSet Compl.compl Set.instCompl Set.instSingletonSet Set.instMembership	—	IsOpen.mem_nhdsSet isOpen_compl_singleton Set.subset_compl_singleton_iff
compl_singleton_mem_nhds_iff 📖	mathematical	—	Set Filter Filter.instMembership nhds Compl.compl Set.instCompl Set.instSingletonSet	—	IsOpen.mem_nhds_iff isOpen_compl_singleton
continuousAt_of_tendsto_nhds 📖	mathematical	Filter.Tendsto nhds	ContinuousAt	—	ContinuousAt.eq_1 eq_of_tendsto_nhds
continuousAt_update_of_ne 📖	mathematical	—	ContinuousAt Function.update	—	continuousWithinAt_update_of_ne
continuousOn_update_iff 📖	mathematical	—	ContinuousOn Function.update Set Set.instSDiff Set.instSingletonSet Filter.Tendsto nhdsWithin nhds	—	ContinuousOn.eq_1 and_forall_ne ContinuousWithinAt.mono continuousWithinAt_update_of_ne Set.diff_subset ContinuousWithinAt.mono_of_mem_nhdsWithin inter_mem_nhdsWithin IsOpen.mem_nhds isOpen_ne continuousWithinAt_update_same
continuousWithinAt_congr_set' 📖	mathematical	Filter.EventuallyEq nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	ContinuousWithinAt	—	continuousWithinAt_insert_self continuousWithinAt_congr_set eventuallyEq_insert
continuousWithinAt_diff_singleton 📖	mathematical	—	ContinuousWithinAt Set Set.instSDiff Set.instSingletonSet	—	continuousWithinAt_insert Set.insert_diff_singleton
continuousWithinAt_insert 📖	mathematical	—	ContinuousWithinAt Set Set.instInsert	—	eq_or_ne continuousWithinAt_insert_self nhdsWithin_insert_of_ne
continuousWithinAt_update_of_ne 📖	mathematical	—	ContinuousWithinAt Function.update	—	Filter.EventuallyEq.congr_continuousWithinAt mem_nhdsWithin_of_mem_nhds Filter.mem_of_superset IsOpen.mem_nhds isOpen_ne Function.update_of_ne
disjoint_nhdsWithin_of_mem_discrete 📖	mathematical	IsDiscrete Set Set.instMembership	Filter Filter.instMembership nhdsWithin Compl.compl Set.instCompl Set.instSingletonSet Disjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	nhds_inter_eq_singleton_of_mem_discrete inter_mem_nhdsWithin Set.disjoint_iff_inter_eq_empty Set.inter_assoc Set.compl_inter_self
disjoint_nhds_nhds_iff_not_inseparable 📖	mathematical	—	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhds Inseparable	—	disjoint_nhds_nhds_iff_not_specializes specializes_iff_inseparable instR0Space
disjoint_nhds_nhds_iff_not_specializes 📖	mathematical	—	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhds Specializes	—	Specializes.not_disjoint R1Space.specializes_or_disjoint_nhds
disjoint_nhds_pure 📖	mathematical	—	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhds Filter.instPure	—	t1Space_iff_disjoint_nhds_pure
disjoint_pure_nhds 📖	mathematical	—	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter Filter.instPure nhds	—	t1Space_iff_disjoint_pure_nhds
eq_of_tendsto_nhds 📖	—	Filter.Tendsto nhds	—	—	by_contra compl_singleton_mem_nhds Filter.Tendsto.comp Filter.tendsto_id' pure_le_nhds
eventuallyEq_insert 📖	mathematical	Filter.EventuallyEq nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	nhds Set.instInsert	—	Set.compl_union_self nhdsWithin_union nhdsWithin_singleton Set.union_singleton Filter.mp_mem nhdsWithin_compl_singleton_le Filter.univ_mem'
eventually_ne_nhds 📖	mathematical	—	Filter.Eventually nhds	—	IsOpen.eventually_mem isOpen_ne
eventually_ne_nhdsWithin 📖	mathematical	—	Filter.Eventually nhdsWithin	—	Filter.Eventually.filter_mono nhdsWithin_le_nhds eventually_ne_nhds
eventually_nhdsNE_eventually_nhds_iff 📖	mathematical	—	Filter.Eventually nhds nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	—	eventually_nhdsWithin_eventually_nhds_iff_of_isOpen isOpen_ne
eventually_nhdsWithin_eventually_nhds_iff_of_isOpen 📖	mathematical	IsOpen	Filter.Eventually nhds nhdsWithin	—	eventually_eventually_nhdsWithin Filter.mp_mem Filter.univ_mem' eventually_nhdsWithin_of_eventually_nhds eventually_nhdsWithin_of_forall IsOpen.nhdsWithin_eq
exists_isCompact_superset_iff 📖	mathematical	—	IsCompact Set Set.instHasSubset closure	—	IsCompact.closure_of_subset subset_closure
exists_isOpen_mem_isCompact_closure 📖	mathematical	—	IsOpen Set Set.instMembership IsCompact closure	—	exists_isOpen_superset_and_isCompact_closure isCompact_singleton
exists_isOpen_singleton_of_isOpen_finite 📖	mathematical	Set.Nonempty IsOpen	Set Set.instMembership Set.instSingletonSet	—	CanLift.prf Set.instCanLiftFinsetCoeFinite em minimal_nonempty_open_eq_singleton of_not_not Set.Finite.subset Finset.finite_toSet ssubset_iff_subset_ne Finset.instIsNonstrictStrictOrderSubsetSSubset Finset.instAntisymmSubset
exists_isOpen_superset_and_isCompact_closure 📖	mathematical	IsCompact	IsOpen Set Set.instHasSubset closure	—	exists_compact_superset isOpen_interior IsCompact.closure_of_subset interior_subset
exists_isOpen_xor'_mem 📖	mathematical	—	IsOpen Xor' Set Set.instMembership	—	t0Space_iff_exists_isOpen_xor'_mem
exists_mem_nhds_isCompact_isClosed 📖	mathematical	—	Set Filter Filter.instMembership nhds IsCompact IsClosed	—	Filter.HasBasis.ex_mem isCompact_isClosed_basis_nhds
exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds 📖	mathematical	Continuous Set Filter Filter.instMembership nhds IsCompact	Set.MapsTo	—	IsCompact.diff IsCompact.image isOpen_interior nhdsSet_singleton IsCompact.disjoint_nhdsSet_right Inseparable.mem_open_iff mem_interior_iff_mem_nhds Filter.diff_mem Filter.mp_mem Continuous.continuousAt IsOpen.mem_nhds Filter.univ_mem' Set.disjoint_left IsOpen.preimage Set.mem_image_of_mem Set.notMem_subset interior_subset
exists_open_singleton_of_finite 📖	mathematical	—	IsOpen Set Set.instSingletonSet	—	exists_isOpen_singleton_of_isOpen_finite Set.toFinite Subtype.finite Set.univ_nonempty isOpen_univ
infinite_of_mem_nhds 📖	mathematical	Set Filter Filter.instMembership nhds	Set.Infinite	—	Filter.NeBot.ne' isOpen_singleton_iff_punctured_nhds isOpen_singleton_of_finite_mem_nhds
injective_nhdsSet 📖	mathematical	—	Set Filter nhdsSet	—	nhdsSet_inj_iff
inseparable_eq_eq 📖	mathematical	—	Inseparable	—	inseparable_iff_eq
inseparable_iff_eq 📖	mathematical	—	Inseparable	—	nhds_injective
insert_mem_nhdsWithin_of_subset_insert 📖	mathematical	Set Set.instHasSubset Set.instInsert	Filter Filter.instMembership nhdsWithin	—	eq_or_ne Filter.mem_of_superset self_mem_nhdsWithin nhdsWithin_mono nhdsWithin_insert_of_ne Set.subset_insert
instLocallyCompactPairOfWeaklyLocallyCompactSpaceOfR1Space 📖	mathematical	—	LocallyCompactPair	—	WeaklyLocallyCompactSpace.exists_compact_mem_nhds exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds
instR0Space 📖	mathematical	—	R0Space	—	R1Space.specializes_or_disjoint_nhds Specializes.not_disjoint Disjoint.symm
instR0SpaceForall 📖	mathematical	R0Space	Pi.topologicalSpace	—	specializes_pi Specializes.symm
instR0SpaceOfT1Space 📖	mathematical	—	R0Space	—	t1Space_iff_t0Space_and_r0Space
instR0SpaceProd 📖	mathematical	—	R0Space instTopologicalSpaceProd	—	Specializes.prod Specializes.symm Specializes.fst Specializes.snd
instR0SpaceSubtype 📖	mathematical	—	R0Space instTopologicalSpaceSubtype	—	Topology.IsInducing.r0Space Topology.IsInducing.subtypeVal
instR1SpaceForall 📖	mathematical	R1Space	Pi.topologicalSpace	—	R1Space.iInf R1Space.induced
instR1SpaceProd 📖	mathematical	—	R1Space instTopologicalSpaceProd	—	R1Space.inf R1Space.induced
instR1SpaceSubtype 📖	mathematical	—	R1Space instTopologicalSpaceSubtype	—	R1Space.induced
instT1SpaceCofiniteTopology 📖	mathematical	—	T1Space CofiniteTopology CofiniteTopology.instTopologicalSpace	—	t1Space_iff_continuous_cofinite_of continuous_id
instT1SpaceForall 📖	mathematical	T1Space	Pi.topologicalSpace	—	isClosed_set_pi isClosed_singleton Set.univ_pi_singleton
instT1SpaceOfDiscreteTopology 📖	mathematical	—	T1Space	—	isClosed_discrete
instT1SpaceOfT0SpaceOfR0Space 📖	mathematical	—	T1Space	—	t1Space_iff_t0Space_and_r0Space
instT1SpaceProd 📖	mathematical	—	T1Space instTopologicalSpaceProd	—	IsClosed.prod isClosed_singleton Set.singleton_prod_singleton
isClosedEmbedding_update 📖	mathematical	T1Space	Topology.IsClosedEmbedding Pi.topologicalSpace Function.update	—	Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap Continuous.update continuous_const continuous_id Function.update_injective Set.update_image isClosed_set_pi
isClosedMap_const 📖	mathematical	—	IsClosedMap	—	IsClosedMap.of_nonempty Set.image_congr Set.Nonempty.image_const
isClosedMap_prodMk_left 📖	mathematical	—	IsClosedMap instTopologicalSpaceProd	—	IsClosed.prod isClosed_singleton Set.singleton_prod
isClosedMap_prodMk_right 📖	mathematical	—	IsClosedMap instTopologicalSpaceProd	—	IsClosed.prod isClosed_singleton Set.prod_singleton
isClosed_inter_singleton 📖	mathematical	—	IsClosed Set Set.instInter Set.instSingletonSet	—	Set.Subsingleton.isClosed Set.Subsingleton.inter_singleton
isClosed_setOf_inseparable 📖	mathematical	—	IsClosed instTopologicalSpaceProd setOf Inseparable	—	instR0Space
isClosed_setOf_specializes 📖	mathematical	—	IsClosed instTopologicalSpaceProd setOf Specializes	—	—
isClosed_singleton 📖	mathematical	—	IsClosed Set Set.instSingletonSet	—	T1Space.t1
isClosed_singleton_inter 📖	mathematical	—	IsClosed Set Set.instInter Set.instSingletonSet	—	Set.Subsingleton.isClosed Set.Subsingleton.singleton_inter
isCompact_closure_singleton 📖	mathematical	—	IsCompact closure Set Set.instSingletonSet	—	isCompact_of_finite_subcover Set.mem_iUnion subset_closure Set.iUnion_congr_Prop Set.iUnion_iUnion_eq_left Specializes.mem_open specializes_comm specializes_iff_mem_closure
isCompact_isClosed_basis_nhds 📖	mathematical	—	Filter.HasBasis Set nhds Filter Filter.instMembership IsCompact IsClosed	—	WeaklyLocallyCompactSpace.exists_compact_mem_nhds IsCompact.isCompact_isClosed_basis_nhds
isEmbedding_iff_isInducing 📖	mathematical	—	Topology.IsEmbedding Topology.IsInducing	—	Topology.IsEmbedding.isInducing Topology.IsInducing.isEmbedding
isOpen_compl_singleton 📖	mathematical	—	IsOpen Compl.compl Set Set.instCompl Set.instSingletonSet	—	IsClosed.isOpen_compl isClosed_singleton
isOpen_inter_eq_singleton_of_mem_discrete 📖	mathematical	IsDiscrete Set Set.instMembership	IsOpen Set.instInter Set.instSingletonSet	—	nhds_inter_eq_singleton_of_mem_discrete mem_nhds_iff
isOpen_ne 📖	mathematical	—	IsOpen setOf	—	isOpen_compl_singleton
isOpen_setOf_eventually_nhdsWithin 📖	mathematical	—	IsOpen setOf Filter.Eventually nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	—	isOpen_iff_mem_nhds Filter.mp_mem eventually_nhds_nhdsWithin Filter.univ_mem' eq_or_ne Filter.Eventually.filter_mono nhdsWithin_le_nhds Ne.nhdsWithin_compl_singleton
isOpen_singleton_of_finite_mem_nhds 📖	mathematical	Set Filter Filter.instMembership nhds	IsOpen Set.instSingletonSet	—	mem_of_mem_nhds Set.Finite.isClosed Set.Finite.subset Set.diff_subset IsOpen.mem_nhds IsClosed.isOpen_compl Set.diff_diff_cancel_left Filter.inter_mem subset_interior_iff_isOpen Set.singleton_subset_iff mem_interior_iff_mem_nhds
ker_nhds 📖	mathematical	—	Filter.ker nhds Set Set.instSingletonSet	—	ker_nhds_eq_specializes specializes_eq_eq
minimal_nonempty_closed_eq_singleton 📖	mathematical	Set.Nonempty	Set Set.instSingletonSet	—	Set.exists_eq_singleton_iff_nonempty_subsingleton minimal_nonempty_closed_subsingleton
minimal_nonempty_closed_subsingleton 📖	mathematical	—	Set.Subsingleton	—	of_not_not exists_isOpen_xor'_mem Set.diff_subset IsClosed.sdiff Eq.subset Set.instReflSubset
minimal_nonempty_open_eq_singleton 📖	mathematical	IsOpen Set.Nonempty	Set Set.instSingletonSet	—	Set.exists_eq_singleton_iff_nonempty_subsingleton minimal_nonempty_open_subsingleton
minimal_nonempty_open_subsingleton 📖	mathematical	IsOpen	Set.Subsingleton	—	of_not_not exists_isOpen_xor'_mem Set.inter_subset_left IsOpen.inter Eq.subset Set.instReflSubset
nhdsNE_le_cofinite 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet Filter.cofinite	—	Filter.le_cofinite_iff_compl_singleton_mem eq_or_ne self_mem_nhdsWithin eventually_ne_nhdsWithin
nhdsSet_inj_iff 📖	mathematical	—	nhdsSet	—	nhdsSet_le_iff
nhdsSet_le_iff 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhdsSet Set Set.instHasSubset	—	monotone_nhdsSet
nhdsWithin_compl_singleton_le 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	—	eq_or_ne Eq.le Ne.nhdsWithin_compl_singleton nhdsWithin_le_nhds
nhdsWithin_insert_of_ne 📖	mathematical	—	nhdsWithin Set Set.instInsert	—	le_antisymm Filter.le_def mem_nhdsWithin IsOpen.sdiff isClosed_singleton Set.inter_insert_of_notMem Set.notMem_diff_of_mem Set.mem_singleton HasSubset.Subset.trans Set.instIsTransSubset Set.inter_subset_inter Set.diff_subset Set.Subset.rfl nhdsWithin_mono Set.subset_insert
nhdsWithin_of_mem_discrete 📖	mathematical	IsDiscrete Set Set.instMembership	nhdsWithin Filter Filter.instPure	—	LE.le.antisymm Filter.le_pure_iff singleton_mem_nhdsWithin_of_mem_discrete pure_le_nhdsWithin
nhds_eq_nhds_iff 📖	mathematical	—	nhds	—	nhds_injective
nhds_injective 📖	mathematical	—	Filter nhds	—	t0Space_iff_nhds_injective
nhds_inter_eq_singleton_of_mem_discrete 📖	mathematical	IsDiscrete Set Set.instMembership	Filter Filter.instMembership nhds Set.instInter Set.instSingletonSet	—	Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete Filter.basis_sets
nhds_le_nhdsSet_iff 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds nhdsSet Set Set.instMembership	—	nhdsSet_singleton nhdsSet_le_iff Set.singleton_subset_iff
nhds_le_nhds_iff 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds	—	specializes_iff_eq
pure_le_nhds_iff 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.instPure nhds	—	specializes_iff_pure specializes_iff_eq
r0Space_iff 📖	mathematical	—	R0Space Symmetric Specializes	—	—
r1Space_iff_inseparable_or_disjoint_nhds 📖	mathematical	—	R1Space Inseparable Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhds	—	Specializes.inseparable instR0Space R1Space.specializes_or_disjoint_nhds Inseparable.specializes
r1Space_iff_specializes_or_disjoint_nhds 📖	mathematical	—	R1Space Specializes Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhds	—	—
r1_separation 📖	mathematical	Inseparable	IsOpen Set Set.instMembership Disjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	Filter.HasBasis.disjoint_iff nhds_basis_opens disjoint_nhds_nhds_iff_not_inseparable
singleton_mem_nhdsWithin_of_mem_discrete 📖	mathematical	IsDiscrete Set Set.instMembership	Filter Filter.instMembership nhdsWithin Set.instSingletonSet	—	nhds_discrete isDiscrete_iff_discreteTopology nhdsWithin_eq_map_subtype_coe Set.image_singleton Filter.image_mem_map
specializes_comm 📖	mathematical	—	Specializes	—	Specializes.symm
specializes_eq_eq 📖	mathematical	—	Specializes	—	specializes_iff_eq
specializes_iff_eq 📖	mathematical	—	Specializes	—	Specializes.eq specializes_rfl
specializes_iff_inseparable 📖	mathematical	—	Specializes Inseparable	—	Specializes.antisymm Specializes.symm Inseparable.specializes
specializes_iff_not_disjoint 📖	mathematical	—	Specializes Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhds	—	Iff.not_left disjoint_nhds_nhds_iff_not_specializes
strictMono_nhdsSet 📖	mathematical	—	StrictMono Set Filter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Filter.instPartialOrder nhdsSet	—	Monotone.strictMono_of_injective monotone_nhdsSet injective_nhdsSet
subsingleton_closure 📖	mathematical	—	Set.Subsingleton closure	—	Set.Subsingleton.anti subset_closure Set.Subsingleton.closure
t0Space_iff_exists_isOpen_xor'_mem 📖	mathematical	—	T0Space Pairwise Set IsOpen Xor' Set.instMembership	—	—
t0Space_iff_inseparable 📖	mathematical	—	T0Space	—	—
t0Space_iff_nhds_injective 📖	mathematical	—	T0Space Filter nhds	—	t0Space_iff_inseparable
t0Space_iff_not_inseparable 📖	mathematical	—	T0Space Pairwise Inseparable	—	—
t0Space_iff_or_notMem_closure 📖	mathematical	—	T0Space Pairwise Set Set.instMembership closure Set.instSingletonSet	—	—
t0Space_of_injective_of_continuous 📖	mathematical	Continuous	T0Space	—	Inseparable.eq Inseparable.map
t1Space_TFAE 📖	mathematical	—	List.TFAE T1Space Continuous CofiniteTopology CofiniteTopology.instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike CofiniteTopology.of T0Space R0Space	—	T1Space.t1 forall_swap Filter.HasBasis.mem_iff nhds_basis_opens isOpen_empty IsClosed.isOpen_compl Set.Finite.isClosed compl_compl IsClosed.preimage CofiniteTopology.isClosed_iff Set.finite_singleton Inseparable.specializes specializes_of_eq Inseparable.eq Specializes.antisymm Specializes.symm List.tfae_of_cycle
t1Space_antitone 📖	mathematical	—	Antitone TopologicalSpace PartialOrder.toPreorder TopologicalSpace.instPartialOrder Prop.partialOrder T1Space	—	IsClosed.mono T1Space.t1
t1Space_iff_continuous_cofinite_of 📖	mathematical	—	T1Space Continuous CofiniteTopology CofiniteTopology.instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike CofiniteTopology.of	—	List.TFAE.out t1Space_TFAE
t1Space_iff_disjoint_nhds_pure 📖	mathematical	—	T1Space Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhds Filter.instPure	—	List.TFAE.out t1Space_TFAE
t1Space_iff_disjoint_pure_nhds 📖	mathematical	—	T1Space Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter Filter.instPure nhds	—	List.TFAE.out t1Space_TFAE
t1Space_iff_exists_open 📖	mathematical	—	T1Space Pairwise Set IsOpen Set.instMembership	—	List.TFAE.out t1Space_TFAE
t1Space_iff_specializes_imp_eq 📖	mathematical	—	T1Space	—	List.TFAE.out t1Space_TFAE
t1Space_iff_t0Space_and_r0Space 📖	mathematical	—	T1Space T0Space R0Space	—	List.TFAE.out t1Space_TFAE
t1Space_of_injective_of_continuous 📖	mathematical	Continuous	T1Space	—	t1Space_iff_specializes_imp_eq Specializes.eq Specializes.map
tendsto_const_nhds_iff 📖	mathematical	—	Filter.Tendsto nhds	—	Filter.map_const
tendsto_nhds_unique_inseparable 📖	mathematical	Filter.Tendsto nhds	Inseparable	—	Inseparable.of_nhds_neBot Filter.neBot_of_le Filter.map_neBot le_inf

---

← Back to Index