Inseparable

📁 Source: Mathlib/Topology/Inseparable.lean

Statistics

Metric	Count
Definitions GeneralizingMap, Inseparable, instInhabited, instOne, instZero, lift₂, mk, SpecializingMap, StableUnderGeneralization, StableUnderSpecialization, instTopologicalSpaceSeparationQuotient	11
Theorems specialization_monotone, specializes_iff, comp, stableUnderGeneralization_image, stableUnderGeneralization_range, GeneralizingMap_iff_stableUnderGeneralization_image, map, map_of_continuousAt, map_of_continuousOn, map_of_continuousWithinAt, mem_closed_iff, mem_open_iff, nhds_eq, of_eq, prod, refl, rfl, specializes, specializes', trans, continuous_piecewise_of_specializes, not_inseparable, not_specializes, stableUnderSpecialization, specializingMap, of_subset_of_specializes, continuous_piecewise_of_specializes, not_inseparable, not_specializes, stableUnderGeneralization, generalizingMap, comap_mk_nhdsSet, comap_mk_nhdsSet_image, comap_mk_nhds_mk, continuousAt_lift, continuousAt_lift₂, continuousOn_lift, continuousOn_lift₂, continuousWithinAt_lift, continuousWithinAt_lift₂, continuous_lift, continuous_lift₂, continuous_mk, exists, forall, image_mk_closure, inseparableSetoid_eq_top_iff, instNonempty, instNontrivialOfNontrivialTopology, instSubsingleton, instSubsingletonOfIndiscreteTopology, isClosedMap_mk, isInducing_mk, isOpenMap_mk, isOpenQuotientMap_mk, isQuotientMap_mk, isQuotientMap_prodMap_mk, lift_comp_mk, lift_mk, lift₂_mk, map_mk_nhds, map_mk_nhdsSet, map_mk_nhdsWithin_preimage, map_prod_map_mk_nhds, mk_eq_mk, mk_one, mk_zero, nontrivial_iff, preimage_image_mk_closed, preimage_image_mk_open, preimage_mk_closure, preimage_mk_frontier, preimage_mk_interior, range_mk, subsingleton_iff, surjective_mk, tendsto_lift_nhdsWithin_mk, tendsto_lift_nhds_mk, tendsto_lift₂_nhds, tendsto_lift₂_nhdsWithin, antisymm, closure_subset, clusterPt, fst, map, map_of_continuousAt, map_of_continuousOn, map_of_continuousWithinAt, mem_closed, mem_closure, mem_open, nhds_le_nhds, not_disjoint, of_eq, prod, pure_le_nhds, snd, trans, closure_singleton_subset, comp, stableUnderSpecialization_image, stableUnderSpecialization_range, compl, image, preimage, Union_eq, compl, image, preimage, generalizingMap, inseparable_iff, specializes_iff, specializingMap, Union_closure_singleton_eq_iff, closure_singleton_eq_Iic, continuous_congr_of_inseparable, inseparable_def, inseparable_iff_closure_eq, inseparable_iff_forall_isClosed, inseparable_iff_forall_isOpen, inseparable_iff_mem_closure, inseparable_iff_specializes_and, inseparable_of_nhdsWithin_eq, inseparable_pi, inseparable_prod, ker_nhds_eq_specializes, not_inseparable_iff_exists_open, not_specializes_iff_exists_closed, not_specializes_iff_exists_open, specializes_TFAE, specializes_iff_closure_subset, specializes_iff_clusterPt, specializes_iff_forall_closed, specializes_iff_forall_open, specializes_iff_mem_closure, specializes_iff_nhds, specializes_iff_pure, specializes_of_eq, specializes_of_nhdsWithin, specializes_pi, specializes_prod, specializes_refl, specializes_rfl, specializingMap_iff_closure_singleton, specializingMap_iff_closure_singleton_subset, specializingMap_iff_isClosed_image_closure_singleton, specializingMap_iff_stableUnderSpecialization_image, specializingMap_iff_stableUnderSpecialization_image_singleton, stableUnderGeneralization_compl_iff, stableUnderGeneralization_empty, stableUnderGeneralization_iInter, stableUnderGeneralization_iUnion, stableUnderGeneralization_iff_exists_sInter_eq, stableUnderGeneralization_sInter, stableUnderGeneralization_sUnion, stableUnderGeneralization_univ, stableUnderSpecialization_compl_iff, stableUnderSpecialization_empty, stableUnderSpecialization_iInter, stableUnderSpecialization_iUnion, stableUnderSpecialization_iff_Union_eq, stableUnderSpecialization_iff_exists_sUnion_eq, stableUnderSpecialization_sInter, stableUnderSpecialization_sUnion, stableUnderSpecialization_univ, subtype_inseparable_iff, subtype_specializes_iff	167
Total	178

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
specialization_monotone 📖	mathematical	Continuous	Monotone specializationPreorder	—	Specializes.map

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
specializes_iff 📖	mathematical	Filter.HasBasis nhds	Specializes Set Set.instMembership	—	specializes_iff_pure ge_iff

GeneralizingMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	—	GeneralizingMap	—	—	Set.image_comp
stableUnderGeneralization_image 📖	mathematical	GeneralizingMap StableUnderGeneralization	Set.image	—	IsUpperSet.image_fibration
stableUnderGeneralization_range 📖	mathematical	GeneralizingMap	StableUnderGeneralization Set.range	—	StableUnderGeneralization.image stableUnderGeneralization_univ Set.image_univ

Inseparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map 📖	—	Inseparable Continuous	—	—	map_of_continuousAt Continuous.continuousAt
map_of_continuousAt 📖	—	Inseparable ContinuousAt	—	—	map_of_continuousWithinAt ContinuousAt.continuousWithinAt Set.mem_univ
map_of_continuousOn 📖	—	Inseparable ContinuousOn Set Set.instMembership	—	—	map_of_continuousWithinAt ContinuousOn.continuousWithinAt
map_of_continuousWithinAt 📖	—	Inseparable ContinuousWithinAt Set Set.instMembership	—	—	Specializes.antisymm Specializes.map_of_continuousWithinAt specializes specializes'
mem_closed_iff 📖	mathematical	Inseparable	Set Set.instMembership	—	inseparable_iff_forall_isClosed
mem_open_iff 📖	mathematical	Inseparable IsOpen	Set Set.instMembership	—	inseparable_iff_forall_isOpen
nhds_eq 📖	mathematical	Inseparable	nhds	—	—
of_eq 📖	mathematical	—	Inseparable	—	refl
prod 📖	mathematical	Inseparable	instTopologicalSpaceProd	—	inseparable_prod
refl 📖	mathematical	—	Inseparable	—	—
rfl 📖	mathematical	—	Inseparable	—	refl
specializes 📖	mathematical	Inseparable	Specializes	—	Eq.le
specializes' 📖	mathematical	Inseparable	Specializes	—	Eq.ge
trans 📖	—	Inseparable	—	—	—

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_piecewise_of_specializes 📖	mathematical	Continuous Specializes	Set.piecewise	—	Set.piecewise_compl IsOpen.continuous_piecewise_of_specializes isOpen_compl
not_inseparable 📖	mathematical	Set Set.instMembership	Inseparable	—	Inseparable.mem_closed_iff
not_specializes 📖	mathematical	Set Set.instMembership	Specializes	—	Specializes.mem_closed
stableUnderSpecialization 📖	mathematical	—	StableUnderSpecialization	—	Specializes.mem_closed

IsClosedMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
specializingMap 📖	mathematical	IsClosedMap	SpecializingMap	—	specializingMap_iff_stableUnderSpecialization_image_singleton IsClosed.stableUnderSpecialization isClosed_closure

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_subset_of_specializes 📖	—	IsCompact Set Set.instHasSubset Set.instMembership Specializes	—	—	LE.le.trans Filter.monotone_principal Specializes.clusterPt

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_piecewise_of_specializes 📖	mathematical	IsOpen Continuous Specializes	Set.piecewise	—	Specializes.mem_open continuous_def Set.piecewise_preimage Set.ite_eq_of_subset_right union inter preimage
not_inseparable 📖	mathematical	IsOpen Set Set.instMembership	Inseparable	—	Inseparable.mem_open_iff
not_specializes 📖	mathematical	IsOpen Set Set.instMembership	Specializes	—	Specializes.mem_open
stableUnderGeneralization 📖	mathematical	IsOpen	StableUnderGeneralization	—	Specializes.mem_open

IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
generalizingMap 📖	mathematical	Topology.IsOpenEmbedding	GeneralizingMap	—	Topology.IsInducing.generalizingMap Topology.IsOpenEmbedding.isInducing IsOpen.stableUnderGeneralization Topology.IsOpenEmbedding.isOpen_range

SeparationQuotient

Definitions

Name	Category	Theorems
instInhabited 📖	CompOp	—
instOne 📖	CompOp	3 math math: instNormOneClass, mk_one, mk_eq_one_iff
instZero 📖	CompOp	3 math math: instIsBoundedSMulSeparationQuotient, mk_eq_zero_iff, mk_zero
lift₂ 📖	CompOp	8 math math: tendsto_lift₂_nhds, tendsto_lift₂_nhdsWithin, continuousAt_lift₂, uniformContinuous_uncurry_lift₂, lift₂_mk, continuousWithinAt_lift₂, continuousOn_lift₂, continuous_lift₂
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_mk_nhdsSet 📖	mathematical	—	Filter.comap SeparationQuotient nhdsSet instTopologicalSpaceSeparationQuotient Set.preimage	—	Set.image_preimage_eq comap_mk_nhdsSet_image
comap_mk_nhdsSet_image 📖	mathematical	—	Filter.comap SeparationQuotient nhdsSet instTopologicalSpaceSeparationQuotient Set.image	—	Topology.IsInducing.nhdsSet_eq_comap
comap_mk_nhds_mk 📖	mathematical	—	Filter.comap SeparationQuotient nhds instTopologicalSpaceSeparationQuotient	—	Topology.IsInducing.nhds_eq_comap
continuousAt_lift 📖	mathematical	—	ContinuousAt SeparationQuotient instTopologicalSpaceSeparationQuotient lift	—	—
continuousAt_lift₂ 📖	mathematical	—	ContinuousAt SeparationQuotient instTopologicalSpaceProd instTopologicalSpaceSeparationQuotient lift₂	—	tendsto_lift₂_nhds
continuousOn_lift 📖	mathematical	—	ContinuousOn SeparationQuotient instTopologicalSpaceSeparationQuotient lift Set.preimage	—	Function.Surjective.forall
continuousOn_lift₂ 📖	mathematical	—	ContinuousOn SeparationQuotient instTopologicalSpaceProd instTopologicalSpaceSeparationQuotient lift₂ Set.preimage	—	Function.Surjective.forall Function.Surjective.prodMap
continuousWithinAt_lift 📖	mathematical	—	ContinuousWithinAt SeparationQuotient instTopologicalSpaceSeparationQuotient lift Set.preimage	—	—
continuousWithinAt_lift₂ 📖	mathematical	—	ContinuousWithinAt SeparationQuotient instTopologicalSpaceProd instTopologicalSpaceSeparationQuotient lift₂ Set.preimage	—	tendsto_lift₂_nhdsWithin
continuous_lift 📖	mathematical	—	Continuous SeparationQuotient instTopologicalSpaceSeparationQuotient lift	—	—
continuous_lift₂ 📖	mathematical	—	Continuous SeparationQuotient instTopologicalSpaceProd instTopologicalSpaceSeparationQuotient lift₂	—	—
continuous_mk 📖	mathematical	—	Continuous SeparationQuotient instTopologicalSpaceSeparationQuotient	—	—
exists 📖	—	—	—	—	Quotient.exists
forall 📖	—	—	—	—	Quotient.forall
image_mk_closure 📖	mathematical	—	Set.image SeparationQuotient closure instTopologicalSpaceSeparationQuotient	—	HasSubset.Subset.antisymm Set.instAntisymmSubset image_closure_subset_closure_image IsClosedMap.closure_image_subset
inseparableSetoid_eq_top_iff 📖	mathematical	—	inseparableSetoid Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Setoid.completeLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder IndiscreteTopology	—	Setoid.eq_top_iff TopologicalSpace.indiscrete_iff_forall_inseparable
instNonempty 📖	mathematical	—	SeparationQuotient	—	Nonempty.map
instNontrivialOfNontrivialTopology 📖	mathematical	—	Nontrivial SeparationQuotient	—	nontrivial_iff
instSubsingleton 📖	mathematical	—	SeparationQuotient	—	Function.Surjective.subsingleton
instSubsingletonOfIndiscreteTopology 📖	mathematical	—	SeparationQuotient	—	subsingleton_iff
isClosedMap_mk 📖	mathematical	—	IsClosedMap SeparationQuotient instTopologicalSpaceSeparationQuotient	—	Topology.IsInducing.isClosedMap isClosed_univ
isInducing_mk 📖	mathematical	—	Topology.IsInducing SeparationQuotient instTopologicalSpaceSeparationQuotient	—	le_antisymm continuous_iff_le_induced preimage_image_mk_open
isOpenMap_mk 📖	mathematical	—	IsOpenMap SeparationQuotient instTopologicalSpaceSeparationQuotient	—	Topology.IsQuotientMap.isOpen_preimage preimage_image_mk_open
isOpenQuotientMap_mk 📖	mathematical	—	IsOpenQuotientMap SeparationQuotient instTopologicalSpaceSeparationQuotient	—	—
isQuotientMap_mk 📖	mathematical	—	Topology.IsQuotientMap SeparationQuotient instTopologicalSpaceSeparationQuotient	—	—
isQuotientMap_prodMap_mk 📖	mathematical	—	Topology.IsQuotientMap SeparationQuotient instTopologicalSpaceProd instTopologicalSpaceSeparationQuotient	—	IsOpenQuotientMap.isQuotientMap IsOpenQuotientMap.prodMap
lift_comp_mk 📖	mathematical	—	SeparationQuotient lift	—	—
lift_mk 📖	mathematical	—	lift	—	—
lift₂_mk 📖	mathematical	—	lift₂	—	—
map_mk_nhds 📖	mathematical	—	Filter.map SeparationQuotient nhds instTopologicalSpaceSeparationQuotient	—	Filter.map_comap_of_surjective
map_mk_nhdsSet 📖	mathematical	—	Filter.map SeparationQuotient nhdsSet instTopologicalSpaceSeparationQuotient Set.image	—	comap_mk_nhdsSet_image Filter.map_comap_of_surjective
map_mk_nhdsWithin_preimage 📖	mathematical	—	Filter.map SeparationQuotient nhdsWithin Set.preimage instTopologicalSpaceSeparationQuotient	—	nhdsWithin.eq_1 Filter.comap_principal Filter.push_pull map_mk_nhds
map_prod_map_mk_nhds 📖	mathematical	—	Filter.map SeparationQuotient nhds instTopologicalSpaceProd instTopologicalSpaceSeparationQuotient	—	nhds_prod_eq Filter.prod_map_map_eq' map_mk_nhds
mk_eq_mk 📖	mathematical	—	Inseparable	—	Quotient.eq''
mk_one 📖	mathematical	—	SeparationQuotient instOne	—	—
mk_zero 📖	mathematical	—	SeparationQuotient instZero	—	—
nontrivial_iff 📖	mathematical	—	Nontrivial SeparationQuotient NontrivialTopology	—	Iff.not subsingleton_iff
preimage_image_mk_closed 📖	mathematical	—	Set.preimage SeparationQuotient Set.image	—	Set.Subset.antisymm Inseparable.mem_closed_iff Set.subset_preimage_image
preimage_image_mk_open 📖	mathematical	IsOpen	Set.preimage SeparationQuotient Set.image	—	Set.Subset.antisymm Inseparable.mem_open_iff Set.subset_preimage_image
preimage_mk_closure 📖	mathematical	—	Set.preimage SeparationQuotient closure instTopologicalSpaceSeparationQuotient	—	IsOpenMap.preimage_closure_eq_closure_preimage
preimage_mk_frontier 📖	mathematical	—	Set.preimage SeparationQuotient frontier instTopologicalSpaceSeparationQuotient	—	IsOpenMap.preimage_frontier_eq_frontier_preimage
preimage_mk_interior 📖	mathematical	—	Set.preimage SeparationQuotient interior instTopologicalSpaceSeparationQuotient	—	IsOpenMap.preimage_interior_eq_interior_preimage
range_mk 📖	mathematical	—	Set.range SeparationQuotient Set.univ	—	Function.Surjective.range_eq
subsingleton_iff 📖	mathematical	—	SeparationQuotient IndiscreteTopology	—	Quotient.subsingleton_iff inseparableSetoid_eq_top_iff
surjective_mk 📖	mathematical	—	SeparationQuotient	—	Quot.mk_surjective
tendsto_lift_nhdsWithin_mk 📖	mathematical	—	Filter.Tendsto SeparationQuotient lift nhdsWithin instTopologicalSpaceSeparationQuotient Set.preimage	—	—
tendsto_lift_nhds_mk 📖	mathematical	—	Filter.Tendsto SeparationQuotient lift nhds instTopologicalSpaceSeparationQuotient	—	—
tendsto_lift₂_nhds 📖	mathematical	—	Filter.Tendsto SeparationQuotient lift₂ nhds instTopologicalSpaceProd instTopologicalSpaceSeparationQuotient	—	map_prod_map_mk_nhds Filter.tendsto_map'_iff
tendsto_lift₂_nhdsWithin 📖	mathematical	—	Filter.Tendsto SeparationQuotient lift₂ nhdsWithin instTopologicalSpaceProd instTopologicalSpaceSeparationQuotient Set.preimage	—	nhdsWithin.eq_1 map_prod_map_mk_nhds Filter.push_pull Filter.comap_principal

Specializes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antisymm 📖	mathematical	Specializes	Inseparable	—	le_antisymm
closure_subset 📖	mathematical	Specializes	Set Set.instHasSubset closure Set.instSingletonSet	—	specializes_iff_closure_subset
clusterPt 📖	mathematical	Specializes	ClusterPt	—	Filter.NeBot.mono inf_le_inf_right
fst 📖	—	Specializes instTopologicalSpaceProd	—	—	specializes_prod
map 📖	—	Specializes Continuous	—	—	map_of_continuousAt Continuous.continuousAt
map_of_continuousAt 📖	—	Specializes ContinuousAt	—	—	map_of_continuousWithinAt ContinuousAt.continuousWithinAt Set.mem_univ
map_of_continuousOn 📖	—	Specializes ContinuousOn Set Set.instMembership	—	—	map_of_continuousWithinAt ContinuousOn.continuousWithinAt
map_of_continuousWithinAt 📖	—	Specializes ContinuousWithinAt Set Set.instMembership	—	—	specializes_iff_pure Filter.map_pure Filter.map_mono le_inf Filter.pure_le_principal ContinuousWithinAt.tendsto
mem_closed 📖	—	Specializes Set Set.instMembership	—	—	specializes_iff_forall_closed
mem_closure 📖	mathematical	Specializes	Set Set.instMembership closure Set.instSingletonSet	—	specializes_iff_mem_closure
mem_open 📖	—	Specializes IsOpen Set Set.instMembership	—	—	specializes_iff_forall_open
nhds_le_nhds 📖	mathematical	Specializes	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds	—	specializes_iff_nhds
not_disjoint 📖	mathematical	Specializes	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhds	—	Disjoint.mono_right nhds_neBot
of_eq 📖	mathematical	—	Specializes	—	specializes_of_eq
prod 📖	mathematical	Specializes	instTopologicalSpaceProd	—	specializes_prod
pure_le_nhds 📖	mathematical	Specializes	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.instPure nhds	—	specializes_iff_pure
snd 📖	—	Specializes instTopologicalSpaceProd	—	—	specializes_prod
trans 📖	—	Specializes	—	—	le_trans

SpecializingMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_singleton_subset 📖	mathematical	SpecializingMap	Set Set.instHasSubset closure Set.instSingletonSet Set.image	—	specializingMap_iff_closure_singleton_subset
comp 📖	—	SpecializingMap	—	—	Set.image_comp
stableUnderSpecialization_image 📖	mathematical	SpecializingMap StableUnderSpecialization	Set.image	—	IsLowerSet.image_fibration
stableUnderSpecialization_range 📖	mathematical	SpecializingMap	StableUnderSpecialization Set.range	—	StableUnderSpecialization.image stableUnderSpecialization_univ Set.image_univ

StableUnderGeneralization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl 📖	mathematical	StableUnderGeneralization	StableUnderSpecialization Compl.compl Set Set.instCompl	—	stableUnderSpecialization_compl_iff
image 📖	mathematical	GeneralizingMap StableUnderGeneralization	Set.image	—	GeneralizingMap.stableUnderGeneralization_image
preimage 📖	mathematical	StableUnderGeneralization Continuous	Set.preimage	—	IsUpperSet.preimage Continuous.specialization_monotone

StableUnderSpecialization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Union_eq 📖	mathematical	StableUnderSpecialization	Set.iUnion Set Set.instMembership closure Set.instSingletonSet	—	stableUnderSpecialization_iff_Union_eq
compl 📖	mathematical	StableUnderSpecialization	StableUnderGeneralization Compl.compl Set Set.instCompl	—	stableUnderGeneralization_compl_iff
image 📖	mathematical	SpecializingMap StableUnderSpecialization	Set.image	—	SpecializingMap.stableUnderSpecialization_image
preimage 📖	mathematical	StableUnderSpecialization Continuous	Set.preimage	—	IsLowerSet.preimage Continuous.specialization_monotone

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
generalizingMap 📖	mathematical	Topology.IsInducing StableUnderGeneralization Set.range	GeneralizingMap	—	specializes_iff
inseparable_iff 📖	mathematical	Topology.IsInducing	Inseparable	—	specializes_iff
specializes_iff 📖	mathematical	Topology.IsInducing	Specializes	—	closure_eq_preimage_closure_image Set.image_singleton
specializingMap 📖	mathematical	Topology.IsInducing StableUnderSpecialization Set.range	SpecializingMap	—	specializes_iff

(root)

Definitions

Name	Category	Theorems
GeneralizingMap 📖	MathDef	11 math math: RingHom.Flat.generalizingMap_comap, TopologicalSpace.IsOpenCover.generalizingMap_iff_comp, AlgebraicGeometry.instIsZariskiLocalAtSourceTopologicallyGeneralizingMap, Topology.IsInducing.generalizingMap, AlgebraicGeometry.Flat.generalizingMap, Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap, GeneralizingMap_iff_stableUnderGeneralization_image, AlgebraicGeometry.instRespectsIsoSchemeTopologicallyGeneralizingMap, AlgebraicGeometry.instIsZariskiLocalAtTargetTopologicallyGeneralizingMap, TopologicalSpace.IsOpenCover.generalizingMap_iff_restrictPreimage, IsOpenEmbedding.generalizingMap
Inseparable 📖	MathDef	63 math math: OnePoint.not_inseparable_infty_coe, SeparationQuotient.mk_eq_mk, inseparable_one_iff_norm, Inseparable.rfl, inseparable_top, group_inseparable_iff, inseparable_iff_specializes_and, TopologicalSpace.eq_top_iff_forall_inseparable, Metric.inseparable_iff, inseparable_pi, IsGenericPoint.inseparable, inseparable_eq_eq, not_inseparable_iff_exists_open, CauchyFilter.cauchyFilter_eq, NontrivialTopology.exists_not_inseparable, Inseparable.of_nhds_neBot, inseparable_def, ContinuousMap.inseparable_coe, Inseparable.of_eq, r1Space_iff_inseparable_or_disjoint_nhds, inseparable_iff_ker_uniformity, IsClosed.not_inseparable, CauchyFilter.inseparable_iff, inseparable_of_nhdsWithin_eq, inseparable_iff_forall_isOpen, isClosed_setOf_inseparable, subtype_inseparable_iff, IsCompact.closure_eq_biUnion_inseparable, TopologicalSpace.nontrivial_iff_exists_not_inseparable, Specializes.antisymm, TopologicalSpace.ne_top_iff_exists_not_inseparable, TopologicalSpace.IsTopologicalBasis.inseparable_iff, inseparable_iff_mem_closure, AbstractCompletion.inseparable_extend_coe, Inseparable.refl, tendsto_nhds_unique_inseparable, Specializes.inseparable, OnePoint.inseparable_coe, disjoint_nhds_nhds_iff_not_inseparable, Inseparable.all, t0Space_iff_not_inseparable, inseparable_iff_eq, inseparable_zero_iff_norm, OnePoint.inseparable_iff, inseparable_iff_forall_isClosed, specializes_iff_inseparable, inseparable_iff_clusterPt_uniformity, inseparable_prod, inseparable_iff_closure_eq, CauchyFilter.inseparable_iff_of_le_nhds, Metric.inseparable_iff_nndist, CauchyFilter.inseparable_lim_iff, TopologicalSpace.indiscrete_iff_forall_inseparable, OnePoint.not_inseparable_coe_infty, Filter.Tendsto.inseparable_iff_uniformity, IsDenseInducing.inseparable_extend, IsCompact.mem_closure_iff_exists_inseparable, EMetric.inseparable_iff, addGroup_inseparable_iff, IsOpen.not_inseparable, Filter.HasBasis.inseparable_iff_uniformity, Topology.IsInducing.inseparable_iff, UniformSpace.Completion.inseparable_extension_coe
SpecializingMap 📖	MathDef	13 math math: AlgebraicGeometry.ValuativeCriterion.Existence.specializingMap, specializingMap_iff_closure_singleton_subset, AlgebraicGeometry.specializingMap_isZariskiLocalAtTarget, AlgebraicGeometry.ValuativeCriterion.Existence.eq, AlgebraicGeometry.specializingMap_respectsIso, specializingMap_iff_stableUnderSpecialization_image, Topology.IsInducing.specializingMap, AlgebraicGeometry.universallyClosed_eq_universallySpecializing, IsClosedMap.specializingMap, specializingMap_iff_isClosed_image_closure_singleton, specializingMap_iff_closure_singleton, specializingMap_iff_stableUnderSpecialization_image_singleton, AlgebraicGeometry.isClosedMap_iff_specializingMap
StableUnderGeneralization 📖	MathDef	11 math math: GeneralizingMap.stableUnderGeneralization_range, stableUnderGeneralization_compl_iff, StableUnderSpecialization.compl, stableUnderSpecialization_compl_iff, stableUnderGeneralization_empty, PrimeSpectrum.stableUnderGeneralization_singleton, stableUnderGeneralization_iff_exists_sInter_eq, stableUnderGeneralization_univ, GeneralizingMap_iff_stableUnderGeneralization_image, PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing, IsOpen.stableUnderGeneralization
StableUnderSpecialization 📖	MathDef	16 math math: SpecializingMap.stableUnderSpecialization_range, stableUnderGeneralization_compl_iff, specializingMap_iff_stableUnderSpecialization_image, PrimeSpectrum.stableUnderSpecialization_range_iff, stableUnderSpecialization_iff_exists_sUnion_eq, IsClosed.stableUnderSpecialization, PrimeSpectrum.stableUnderSpecialization_singleton, stableUnderSpecialization_compl_iff, StableUnderGeneralization.compl, stableUnderSpecialization_univ, Module.stableUnderSpecialization_support, specializingMap_iff_stableUnderSpecialization_image_singleton, stableUnderSpecialization_empty, Union_closure_singleton_eq_iff, stableUnderSpecialization_iff_Union_eq, PrimeSpectrum.stableUnderSpecialization_image_iff
instTopologicalSpaceSeparationQuotient 📖	CompOp	65 math math: SeparationQuotient.t2Space, SeparationQuotient.mkCLM_comp_outCLM, SeparationQuotient.tendsto_lift_nhds_mk, SeparationQuotient.continuous_mk, SeparationQuotient.instNormalSpace, SeparationQuotient.map_mk_nhdsSet, SeparationQuotient.isQuotientMap_prodMap_mk, SeparationQuotient.instContinuousNeg, SeparationQuotient.instIsTopologicalGroup, SeparationQuotient.comap_mk_nhds_mk, SeparationQuotient.tendsto_lift₂_nhds, SeparationQuotient.instContinuousInv, SeparationQuotient.continuousAt_lift, SeparationQuotient.isInducing_mk, SeparationQuotient.continuous_lift, SeparationQuotient.instT0Space, SeparationQuotient.tendsto_lift₂_nhdsWithin, instT3SpaceSeparationQuotientOfRegularSpace, SeparationQuotient.outCLM_uniformContinuous, SeparationQuotient.continuousWithinAt_lift, UniformSpace.topologicalRing, SeparationQuotient.outCLM_isUniformEmbedding, SeparationQuotient.isQuotientMap_mk, SeparationQuotient.image_mk_closure, SeparationQuotient.continuousOn_lift, SeparationQuotient.t1Space_iff, SeparationQuotient.exists_out_continuousLinearMap, SeparationQuotient.mk_outCLM, SeparationQuotient.instContinuousAdd, SeparationQuotient.continuousAt_lift₂, SeparationQuotient.isOpenMap_mk, SeparationQuotient.postcomp_mkCLM_surjective, SeparationQuotient.instContinuousDiv, SeparationQuotient.mk_comp_outCLM, SeparationQuotient.liftContinuousAddCommMonoidHom_mk, SeparationQuotient.preimage_mk_closure, instT5SpaceSeparationQuotientOfCompletelyNormalSpaceOfR0Space, SeparationQuotient.instContinuousConstSMul, SeparationQuotient.liftCLM_apply, SeparationQuotient.isOpenQuotientMap_mk, SeparationQuotient.preimage_mk_interior, SeparationQuotient.liftNormedAddGroupHom_apply, SeparationQuotient.preimage_mk_frontier, SeparationQuotient.comap_mk_nhdsSet_image, SeparationQuotient.instContinuousMul, SeparationQuotient.comap_mk_nhdsSet, SeparationQuotient.continuousWithinAt_lift₂, SeparationQuotient.isEmbedding_outCLM, SeparationQuotient.tendsto_lift_nhdsWithin_mk, SeparationQuotient.map_mk_nhdsWithin_preimage, SeparationQuotient.liftCLM_mk, SeparationQuotient.t2Space_iff, SeparationQuotient.continuousOn_lift₂, SeparationQuotient.continuous_lift₂, SeparationQuotient.map_prod_map_mk_nhds, SeparationQuotient.instContinuousSMul, SeparationQuotient.mkCLM_apply, SeparationQuotient.liftContinuousCommMonoidHom_mk, SeparationQuotient.isClosedMap_mk, SeparationQuotient.map_mk_nhds, SeparationQuotient.instContinuousSub, SeparationQuotient.outCLM_injective, SeparationQuotient.instIsTopologicalAddGroup, SeparationQuotient.instContinuousConstVAdd, SeparationQuotient.outCLM_isUniformInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
GeneralizingMap_iff_stableUnderGeneralization_image 📖	mathematical	—	GeneralizingMap StableUnderGeneralization Set.image	—	Relation.fibration_iff_isUpperSet_image
Union_closure_singleton_eq_iff 📖	mathematical	—	Set.iUnion Set Set.instMembership closure Set.instSingletonSet StableUnderSpecialization	—	Set.iUnion_congr_Prop closure_singleton_eq_Iic coe_lowerClosure
closure_singleton_eq_Iic 📖	mathematical	—	closure Set Set.instSingletonSet Set.Iic specializationPreorder	—	Set.ext specializes_iff_mem_closure
continuous_congr_of_inseparable 📖	mathematical	Inseparable	Continuous	—	Topology.IsInducing.continuous_iff continuous_congr
inseparable_def 📖	mathematical	—	Inseparable nhds	—	—
inseparable_iff_closure_eq 📖	mathematical	—	Inseparable closure Set Set.instSingletonSet	—	Set.instReflSubset Set.instAntisymmSubset
inseparable_iff_forall_isClosed 📖	mathematical	—	Inseparable Set Set.instMembership	—	—
inseparable_iff_forall_isOpen 📖	mathematical	—	Inseparable Set Set.instMembership	—	—
inseparable_iff_mem_closure 📖	mathematical	—	Inseparable Set Set.instMembership closure Set.instSingletonSet	—	inseparable_iff_specializes_and
inseparable_iff_specializes_and 📖	mathematical	—	Inseparable Specializes	—	le_antisymm_iff
inseparable_of_nhdsWithin_eq 📖	mathematical	Set Set.instMembership nhdsWithin	Inseparable	—	Specializes.antisymm specializes_of_nhdsWithin Eq.le Eq.ge
inseparable_pi 📖	mathematical	—	Inseparable Pi.topologicalSpace	—	nhds_pi nhds_neBot
inseparable_prod 📖	mathematical	—	Inseparable instTopologicalSpaceProd	—	nhds_prod_eq nhds_neBot
ker_nhds_eq_specializes 📖	mathematical	—	Filter.ker nhds setOf Specializes	—	Set.ext
not_inseparable_iff_exists_open 📖	mathematical	—	Inseparable IsOpen Xor' Set Set.instMembership	—	—
not_specializes_iff_exists_closed 📖	mathematical	—	Specializes IsClosed Set Set.instMembership	—	specializes_iff_forall_closed Mathlib.Tactic.Push.not_forall_eq
not_specializes_iff_exists_open 📖	mathematical	—	Specializes IsOpen Set Set.instMembership	—	specializes_iff_forall_open Mathlib.Tactic.Push.not_forall_eq
specializes_TFAE 📖	mathematical	—	List.TFAE Specializes Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.instPure nhds Set Set.instMembership closure Set.instSingletonSet Set.instHasSubset ClusterPt	—	LE.le.trans pure_le_nhds IsOpen.mem_nhds of_not_not IsClosed.isOpen_compl isClosed_closure subset_closure Set.mem_singleton IsClosed.closure_subset_iff Set.singleton_subset_iff mem_closure_iff_clusterPt Filter.principal_singleton Filter.HasBasis.ge_iff nhds_basis_opens mem_closure_iff List.tfae_of_cycle
specializes_iff_closure_subset 📖	mathematical	—	Specializes Set Set.instHasSubset closure Set.instSingletonSet	—	List.TFAE.out specializes_TFAE
specializes_iff_clusterPt 📖	mathematical	—	Specializes ClusterPt Filter Filter.instPure	—	List.TFAE.out specializes_TFAE
specializes_iff_forall_closed 📖	mathematical	—	Specializes Set Set.instMembership	—	List.TFAE.out specializes_TFAE
specializes_iff_forall_open 📖	mathematical	—	Specializes Set Set.instMembership	—	List.TFAE.out specializes_TFAE
specializes_iff_mem_closure 📖	mathematical	—	Specializes Set Set.instMembership closure Set.instSingletonSet	—	List.TFAE.out specializes_TFAE
specializes_iff_nhds 📖	mathematical	—	Specializes Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds	—	—
specializes_iff_pure 📖	mathematical	—	Specializes Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.instPure nhds	—	List.TFAE.out specializes_TFAE
specializes_of_eq 📖	mathematical	—	Specializes	—	specializes_refl
specializes_of_nhdsWithin 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhdsWithin Set Set.instMembership	Specializes	—	specializes_iff_pure le_inf pure_le_nhds Filter.le_principal_iff inf_le_left
specializes_pi 📖	mathematical	—	Specializes Pi.topologicalSpace	—	nhds_pi nhds_neBot
specializes_prod 📖	mathematical	—	Specializes instTopologicalSpaceProd	—	nhds_prod_eq nhds_neBot
specializes_refl 📖	mathematical	—	Specializes	—	specializes_rfl
specializes_rfl 📖	mathematical	—	Specializes	—	le_rfl
specializingMap_iff_closure_singleton 📖	mathematical	Continuous	SpecializingMap Set.image closure Set Set.instSingletonSet	—	closure_singleton_eq_Iic Relation.fibration_iff_image_Iic Continuous.specialization_monotone
specializingMap_iff_closure_singleton_subset 📖	mathematical	—	SpecializingMap Set Set.instHasSubset closure Set.instSingletonSet Set.image	—	—
specializingMap_iff_isClosed_image_closure_singleton 📖	mathematical	Continuous	SpecializingMap IsClosed Set.image closure Set Set.instSingletonSet	—	specializingMap_iff_closure_singleton isClosed_closure specializingMap_iff_stableUnderSpecialization_image_singleton IsClosed.stableUnderSpecialization
specializingMap_iff_stableUnderSpecialization_image 📖	mathematical	—	SpecializingMap StableUnderSpecialization Set.image	—	Relation.fibration_iff_isLowerSet_image
specializingMap_iff_stableUnderSpecialization_image_singleton 📖	mathematical	—	SpecializingMap StableUnderSpecialization Set.image closure Set Set.instSingletonSet	—	closure_singleton_eq_Iic Relation.fibration_iff_isLowerSet_image_Iic
stableUnderGeneralization_compl_iff 📖	mathematical	—	StableUnderGeneralization Compl.compl Set Set.instCompl StableUnderSpecialization	—	isUpperSet_compl
stableUnderGeneralization_empty 📖	mathematical	—	StableUnderGeneralization Set Set.instEmptyCollection	—	isUpperSet_empty
stableUnderGeneralization_iInter 📖	mathematical	StableUnderGeneralization	Set.iInter	—	isUpperSet_iInter
stableUnderGeneralization_iUnion 📖	mathematical	StableUnderGeneralization	Set.iUnion	—	isUpperSet_iUnion
stableUnderGeneralization_iff_exists_sInter_eq 📖	mathematical	—	StableUnderGeneralization IsOpen Set.sInter	—	stableUnderSpecialization_compl_iff stableUnderSpecialization_iff_exists_sUnion_eq IsClosed.isOpen_compl compl_injective Set.sUnion_eq_compl_sInter_compl stableUnderGeneralization_sInter IsOpen.stableUnderGeneralization
stableUnderGeneralization_sInter 📖	mathematical	StableUnderGeneralization	Set.sInter	—	isUpperSet_sInter
stableUnderGeneralization_sUnion 📖	mathematical	StableUnderGeneralization	Set.sUnion	—	isUpperSet_sUnion
stableUnderGeneralization_univ 📖	mathematical	—	StableUnderGeneralization Set.univ	—	isUpperSet_univ
stableUnderSpecialization_compl_iff 📖	mathematical	—	StableUnderSpecialization Compl.compl Set Set.instCompl StableUnderGeneralization	—	isLowerSet_compl
stableUnderSpecialization_empty 📖	mathematical	—	StableUnderSpecialization Set Set.instEmptyCollection	—	isLowerSet_empty
stableUnderSpecialization_iInter 📖	mathematical	StableUnderSpecialization	Set.iInter	—	isLowerSet_iInter
stableUnderSpecialization_iUnion 📖	mathematical	StableUnderSpecialization	Set.iUnion	—	isLowerSet_iUnion
stableUnderSpecialization_iff_Union_eq 📖	mathematical	—	StableUnderSpecialization Set.iUnion Set Set.instMembership closure Set.instSingletonSet	—	Union_closure_singleton_eq_iff
stableUnderSpecialization_iff_exists_sUnion_eq 📖	mathematical	—	StableUnderSpecialization IsClosed Set.sUnion	—	isClosed_closure StableUnderSpecialization.Union_eq Set.sUnion_image stableUnderSpecialization_sUnion IsClosed.stableUnderSpecialization
stableUnderSpecialization_sInter 📖	mathematical	StableUnderSpecialization	Set.sInter	—	isLowerSet_sInter
stableUnderSpecialization_sUnion 📖	mathematical	StableUnderSpecialization	Set.sUnion	—	isLowerSet_sUnion
stableUnderSpecialization_univ 📖	mathematical	—	StableUnderSpecialization Set.univ	—	isLowerSet_univ
subtype_inseparable_iff 📖	mathematical	—	Inseparable instTopologicalSpaceSubtype	—	Topology.IsInducing.inseparable_iff Topology.IsInducing.subtypeVal
subtype_specializes_iff 📖	mathematical	—	Specializes instTopologicalSpaceSubtype	—	Topology.IsInducing.specializes_iff Topology.IsInducing.subtypeVal

---

← Back to Index