TopologicalSpace

📁 Source: Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.lean

Statistics

Metric	Count
Definitions homeoBot, homeoTop, topologicalSpace, TopologicalSpace	4
Theorems continuousSMul, continuousVAdd, continuous_coe, continuous_dom, continuous_dom_pi, continuous_dom_prod, continuous_dom_prod_left, continuous_dom_prod_right, continuous_eval, continuous_inclusion, continuous_rng_of_bot, continuous_rng_of_principal, continuous_rng_of_principal_iff_forall, continuous_rng_of_top, instContinuousAddCoeCofinite, instContinuousAddCoePrincipal, instContinuousConstSMulCoe, instContinuousConstVAddCoe, instContinuousInvCoe, instContinuousMulCoeCofinite, instContinuousMulCoePrincipal, instContinuousNegCoe, instContinuousSMulCoePrincipal, instContinuousVAddCoePrincipal, instIsTopologicalAddGroupCoePrincipal, instIsTopologicalGroupCoePrincipal, instIsTopologicalRingCoePrincipal, instLocallyCompactSpaceCoeCofiniteOfAddSubgroupClassOfIsTopologicalAddGroupOfCompactSpaceSubtypeMem, instLocallyCompactSpaceCoeCofiniteOfSubgroupClassOfIsTopologicalGroupOfCompactSpaceSubtypeMem, instT0Space, instT1Space, instT2Space, instWeaklyLocallyCompactSpaceCofiniteOfFactForallIsOpenOfCompactSpaceElem, instWeaklyLocallyCompactSpacePrincipalOfFactLeFilterCofiniteOfCompactSpaceElem, isEmbedding_coe_of_bot, isEmbedding_coe_of_principal, isEmbedding_coe_of_top, isEmbedding_inclusion_principal, isEmbedding_inclusion_top, isEmbedding_structureMap, isOpenEmbedding_inclusion_principal, isOpenEmbedding_structureMap, isOpen_forall_imp_mem, isOpen_forall_imp_mem_of_principal, isOpen_forall_mem, isOpen_forall_mem_of_principal, isTopologicalAddGroup, isTopologicalGroup, isTopologicalRing, locallyCompactSpace_of_addGroup, locallyCompactSpace_of_group, mapAlong_continuous, nhds_eq_map_inclusion, nhds_eq_map_structureMap, nhds_zero_eq_map_ofPre, nhds_zero_eq_map_structureMap, topologicalSpace_eq_iSup, topologicalSpace_eq_of_bot, topologicalSpace_eq_of_principal, topologicalSpace_eq_of_top, weaklyLocallyCompactSpace_of_cofinite, weaklyLocallyCompactSpace_of_principal	62
Total	66

RestrictedProduct

Definitions

Name	Category	Theorems
homeoBot 📖	CompOp	—
homeoTop 📖	CompOp	—
topologicalSpace 📖	CompOp	62 math math: continuous_rng_of_principal, instContinuousMulCoePrincipal, continuous_coe, instLocallyCompactSpaceCoeCofiniteOfSubgroupClassOfIsTopologicalGroupOfCompactSpaceSubtypeMem, nhds_zero_eq_map_ofPre, isOpen_forall_mem_of_principal, isOpenEmbedding_structureMap, instIsTopologicalRingCoePrincipal, instContinuousAddCoePrincipal, isOpen_forall_imp_mem, instWeaklyLocallyCompactSpaceCofiniteOfFactForallIsOpenOfCompactSpaceElem, instIsTopologicalAddGroupCoePrincipal, continuous_dom, continuous_dom_prod, isOpen_forall_mem, continuous_rng_of_top, instWeaklyLocallyCompactSpacePrincipalOfFactLeFilterCofiniteOfCompactSpaceElem, locallyCompactSpace_of_group, isEmbedding_coe_of_principal, instIsTopologicalGroupCoePrincipal, instContinuousNegCoe, nhds_eq_map_structureMap, topologicalSpace_eq_of_principal, weaklyLocallyCompactSpace_of_principal, isTopologicalRing, continuous_inclusion, isEmbedding_inclusion_top, instContinuousConstSMulCoe, instContinuousMulCoeCofinite, continuous_rng_of_principal_iff_forall, instContinuousConstVAddCoe, instContinuousSMulCoePrincipal, continuous_dom_pi, mapAlong_continuous, instT2Space, instLocallyCompactSpaceCoeCofiniteOfAddSubgroupClassOfIsTopologicalAddGroupOfCompactSpaceSubtypeMem, continuous_dom_prod_right, instContinuousAddCoeCofinite, isEmbedding_coe_of_top, instT0Space, continuous_eval, topologicalSpace_eq_of_bot, continuousSMul, locallyCompactSpace_of_addGroup, weaklyLocallyCompactSpace_of_cofinite, isEmbedding_inclusion_principal, isEmbedding_coe_of_bot, topologicalSpace_eq_iSup, nhds_zero_eq_map_structureMap, topologicalSpace_eq_of_top, continuousVAdd, isTopologicalGroup, instContinuousInvCoe, instContinuousVAddCoePrincipal, continuous_rng_of_bot, continuous_dom_prod_left, isTopologicalAddGroup, isOpen_forall_imp_mem_of_principal, isOpenEmbedding_inclusion_principal, instT1Space, nhds_eq_map_inclusion, isEmbedding_structureMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul 📖	mathematical	SMulMemClass ContinuousSMul	ContinuousSMul RestrictedProduct SetLike.coe Filter.cofinite instSMulCoeOfSMulMemClass topologicalSpace	—	continuous_dom_prod_left Fact.out Continuous.comp continuous_inclusion ContinuousSMul.continuous_smul instContinuousSMulCoePrincipal
continuousVAdd 📖	mathematical	VAddMemClass ContinuousVAdd	ContinuousVAdd RestrictedProduct SetLike.coe Filter.cofinite instVAddCoeOfVAddMemClass topologicalSpace	—	continuous_dom_prod_left Fact.out Continuous.comp continuous_inclusion ContinuousVAdd.continuous_vadd instContinuousVAddCoePrincipal
continuous_coe 📖	mathematical	—	Continuous RestrictedProduct topologicalSpace Pi.topologicalSpace DFunLike.coe instDFunLike	—	continuous_iSup_dom continuous_coinduced_dom continuous_induced_dom
continuous_dom 📖	mathematical	—	Continuous RestrictedProduct topologicalSpace Filter.principal inclusion	—	topologicalSpace_eq_of_principal
continuous_dom_pi 📖	mathematical	IsOpen	Continuous Pi.topologicalSpace RestrictedProduct Filter.cofinite topologicalSpace Filter.principal Pi.map inclusion	—	Continuous.comp' Continuous.piMap continuous_inclusion Filter.le_principal_iff nhds_pi nhds_eq_map_inclusion Continuous.tendsto
continuous_dom_prod 📖	mathematical	IsOpen	Continuous RestrictedProduct Filter.cofinite instTopologicalSpaceProd topologicalSpace Filter.principal inclusion	—	continuous_dom_prod_right continuous_dom_prod_left le_inf Filter.inf_principal Filter.principal_mono Set.inter_subset_left Set.inter_subset_right Continuous.comp Continuous.prodMap continuous_inclusion
continuous_dom_prod_left 📖	mathematical	IsOpen	Continuous RestrictedProduct Filter.cofinite instTopologicalSpaceProd topologicalSpace Filter.principal inclusion	—	Continuous.comp Continuous.prodMap continuous_id continuous_inclusion Filter.le_principal_iff exists_inclusion_eq_of_eventually nhds_prod_eq nhds_eq_map_inclusion Filter.map_id Filter.prod_map_map_eq Filter.tendsto_map'_iff Continuous.tendsto
continuous_dom_prod_right 📖	mathematical	IsOpen	Continuous RestrictedProduct Filter.cofinite instTopologicalSpaceProd topologicalSpace Filter.principal inclusion	—	Continuous.comp Continuous.prodMap continuous_inclusion continuous_id Filter.le_principal_iff exists_inclusion_eq_of_eventually nhds_prod_eq nhds_eq_map_inclusion Filter.map_id Filter.prod_map_map_eq Filter.tendsto_map'_iff Continuous.tendsto
continuous_eval 📖	mathematical	—	Continuous RestrictedProduct topologicalSpace DFunLike.coe instDFunLike	—	Continuous.comp continuous_apply continuous_coe
continuous_inclusion 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder	Continuous RestrictedProduct topologicalSpace inclusion	—	coinduced_iSup iSup_congr_Prop coinduced_compose iSup₂_le le_iSup₂_of_le le_trans le_rfl
continuous_rng_of_bot 📖	mathematical	—	Continuous RestrictedProduct Bot.bot Filter Filter.instBot topologicalSpace Pi.topologicalSpace DFunLike.coe instDFunLike	—	Topology.IsEmbedding.continuous_iff isEmbedding_coe_of_bot
continuous_rng_of_principal 📖	mathematical	—	Continuous RestrictedProduct Filter.principal topologicalSpace Pi.topologicalSpace DFunLike.coe instDFunLike	—	Topology.IsEmbedding.continuous_iff isEmbedding_coe_of_principal
continuous_rng_of_principal_iff_forall 📖	mathematical	—	Continuous RestrictedProduct Filter.principal topologicalSpace DFunLike.coe instDFunLike	—	continuous_rng_of_principal continuous_pi_iff
continuous_rng_of_top 📖	mathematical	—	Continuous RestrictedProduct Top.top Filter Filter.instTop topologicalSpace Pi.topologicalSpace DFunLike.coe instDFunLike	—	Topology.IsEmbedding.continuous_iff isEmbedding_coe_of_top
instContinuousAddCoeCofinite 📖	mathematical	AddMemClass ContinuousAdd	ContinuousAdd RestrictedProduct SetLike.coe Filter.cofinite topologicalSpace instAddCoeOfAddMemClass	—	continuous_dom_prod Fact.out Continuous.comp continuous_inclusion continuous_add instContinuousAddCoePrincipal
instContinuousAddCoePrincipal 📖	mathematical	AddMemClass ContinuousAdd	ContinuousAdd RestrictedProduct SetLike.coe Filter.principal topologicalSpace instAddCoeOfAddMemClass	—	Topology.IsInducing.continuousAdd AddHom.addHomClass Pi.continuousAdd Topology.IsEmbedding.toIsInducing isEmbedding_coe_of_principal
instContinuousConstSMulCoe 📖	mathematical	SMulMemClass ContinuousConstSMul	ContinuousConstSMul RestrictedProduct SetLike.coe topologicalSpace instSMulCoeOfSMulMemClass	—	continuous_dom Continuous.comp continuous_inclusion ContinuousConstSMul.continuous_const_smul Topology.IsInducing.continuousConstSMul instContinuousConstSMulForall Topology.IsEmbedding.toIsInducing isEmbedding_coe_of_principal
instContinuousConstVAddCoe 📖	mathematical	VAddMemClass ContinuousConstVAdd	ContinuousConstVAdd RestrictedProduct SetLike.coe topologicalSpace instVAddCoeOfVAddMemClass	—	continuous_dom Continuous.comp continuous_inclusion ContinuousConstVAdd.continuous_const_vadd Topology.IsInducing.continuousConstVAdd instContinuousConstVAddForall Topology.IsEmbedding.toIsInducing isEmbedding_coe_of_principal
instContinuousInvCoe 📖	mathematical	InvMemClass ContinuousInv	ContinuousInv RestrictedProduct SetLike.coe topologicalSpace instInvCoeOfInvMemClass	—	continuous_dom Continuous.comp continuous_inclusion ContinuousInv.continuous_inv Topology.IsInducing.continuousInv Pi.continuousInv Topology.IsEmbedding.toIsInducing isEmbedding_coe_of_principal
instContinuousMulCoeCofinite 📖	mathematical	MulMemClass ContinuousMul	ContinuousMul RestrictedProduct SetLike.coe Filter.cofinite topologicalSpace instMulCoeOfMulMemClass	—	continuous_dom_prod Fact.out Continuous.comp continuous_inclusion continuous_mul instContinuousMulCoePrincipal
instContinuousMulCoePrincipal 📖	mathematical	MulMemClass ContinuousMul	ContinuousMul RestrictedProduct SetLike.coe Filter.principal topologicalSpace instMulCoeOfMulMemClass	—	Topology.IsInducing.continuousMul MulHom.mulHomClass Pi.continuousMul Topology.IsEmbedding.toIsInducing isEmbedding_coe_of_principal
instContinuousNegCoe 📖	mathematical	NegMemClass ContinuousNeg	ContinuousNeg RestrictedProduct SetLike.coe topologicalSpace instNegCoeOfNegMemClass	—	continuous_dom Continuous.comp continuous_inclusion ContinuousNeg.continuous_neg Topology.IsInducing.continuousNeg Pi.continuousNeg Topology.IsEmbedding.toIsInducing isEmbedding_coe_of_principal
instContinuousSMulCoePrincipal 📖	mathematical	SMulMemClass ContinuousSMul	ContinuousSMul RestrictedProduct SetLike.coe Filter.principal instSMulCoeOfSMulMemClass topologicalSpace	—	Topology.IsInducing.continuousSMul instContinuousSMulForall Topology.IsEmbedding.toIsInducing isEmbedding_coe_of_principal continuous_id
instContinuousVAddCoePrincipal 📖	mathematical	VAddMemClass ContinuousVAdd	ContinuousVAdd RestrictedProduct SetLike.coe Filter.principal instVAddCoeOfVAddMemClass topologicalSpace	—	Topology.IsInducing.continuousVAdd instContinuousVAddForall Topology.IsEmbedding.toIsInducing isEmbedding_coe_of_principal continuous_id
instIsTopologicalAddGroupCoePrincipal 📖	mathematical	AddSubgroupClass AddGroup.toSubNegMonoid IsTopologicalAddGroup	IsTopologicalAddGroup RestrictedProduct SetLike.coe Filter.principal topologicalSpace instAddGroupCoeOfAddSubgroupClass	—	instContinuousAddCoePrincipal IsTopologicalAddGroup.toContinuousAdd instContinuousNegCoe IsTopologicalAddGroup.toContinuousNeg
instIsTopologicalGroupCoePrincipal 📖	mathematical	SubgroupClass Group.toDivInvMonoid IsTopologicalGroup	IsTopologicalGroup RestrictedProduct SetLike.coe Filter.principal topologicalSpace instGroupCoeOfSubgroupClass	—	instContinuousMulCoePrincipal IsTopologicalGroup.toContinuousMul instContinuousInvCoe IsTopologicalGroup.toContinuousInv
instIsTopologicalRingCoePrincipal 📖	mathematical	SubringClass Ring.toNonAssocRing IsTopologicalRing NonAssocRing.toNonUnitalNonAssocRing	IsTopologicalRing RestrictedProduct SetLike.coe Filter.principal topologicalSpace NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCoeOfSubringClass	—	instContinuousAddCoePrincipal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instContinuousMulCoePrincipal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instContinuousNegCoe IsSemitopologicalRing.toContinuousNeg
instLocallyCompactSpaceCoeCofiniteOfAddSubgroupClassOfIsTopologicalAddGroupOfCompactSpaceSubtypeMem 📖	mathematical	AddSubgroupClass AddGroup.toSubNegMonoid IsTopologicalAddGroup CompactSpace SetLike.instMembership instTopologicalSpaceSubtype	LocallyCompactSpace RestrictedProduct SetLike.coe Filter.cofinite topologicalSpace	—	locallyCompactSpace_of_addGroup WeaklyLocallyCompactSpace.locallyCompactSpace instR1Space IsTopologicalAddGroup.regularSpace IsCompact.vadd SeparatelyContinuousAdd.to_continuousVAdd instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd isCompact_iff_compactSpace IsOpen.mem_nhds IsOpen.vadd Fact.out add_zero Set.vadd_mem_vadd_set ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass Filter.Eventually.of_forall
instLocallyCompactSpaceCoeCofiniteOfSubgroupClassOfIsTopologicalGroupOfCompactSpaceSubtypeMem 📖	mathematical	SubgroupClass Group.toDivInvMonoid IsTopologicalGroup CompactSpace SetLike.instMembership instTopologicalSpaceSubtype	LocallyCompactSpace RestrictedProduct SetLike.coe Filter.cofinite topologicalSpace	—	locallyCompactSpace_of_group WeaklyLocallyCompactSpace.locallyCompactSpace instR1Space IsTopologicalGroup.regularSpace IsCompact.smul SeparatelyContinuousMul.to_continuousSMul instSeparatelyContinuousMulOfContinuousMul IsTopologicalGroup.toContinuousMul isCompact_iff_compactSpace IsOpen.mem_nhds IsOpen.smul Fact.out mul_one Set.smul_mem_smul_set OneMemClass.one_mem SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Filter.Eventually.of_forall
instT0Space 📖	mathematical	T0Space	T0Space RestrictedProduct topologicalSpace	—	t0Space_of_injective_of_continuous DFunLike.coe_injective continuous_coe Pi.instT0Space
instT1Space 📖	mathematical	T1Space	T1Space RestrictedProduct topologicalSpace	—	t1Space_of_injective_of_continuous DFunLike.coe_injective continuous_coe instT1SpaceForall
instT2Space 📖	mathematical	T2Space	T2Space RestrictedProduct topologicalSpace	—	T2Space.of_injective_continuous Pi.t2Space DFunLike.coe_injective continuous_coe
instWeaklyLocallyCompactSpaceCofiniteOfFactForallIsOpenOfCompactSpaceElem 📖	mathematical	WeaklyLocallyCompactSpace CompactSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	WeaklyLocallyCompactSpace RestrictedProduct Filter.cofinite topologicalSpace	—	weaklyLocallyCompactSpace_of_cofinite Fact.out Filter.Eventually.of_forall isCompact_iff_compactSpace
instWeaklyLocallyCompactSpacePrincipalOfFactLeFilterCofiniteOfCompactSpaceElem 📖	mathematical	WeaklyLocallyCompactSpace CompactSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	WeaklyLocallyCompactSpace RestrictedProduct Filter.principal topologicalSpace	—	weaklyLocallyCompactSpace_of_principal Fact.out isCompact_iff_compactSpace
isEmbedding_coe_of_bot 📖	mathematical	—	Topology.IsEmbedding RestrictedProduct Bot.bot Filter Filter.instBot topologicalSpace Pi.topologicalSpace DFunLike.coe instDFunLike	—	isEmbedding_coe_of_principal Filter.principal_empty
isEmbedding_coe_of_principal 📖	mathematical	—	Topology.IsEmbedding RestrictedProduct Filter.principal topologicalSpace Pi.topologicalSpace DFunLike.coe instDFunLike	—	topologicalSpace_eq_of_principal DFunLike.coe_injective
isEmbedding_coe_of_top 📖	mathematical	—	Topology.IsEmbedding RestrictedProduct Top.top Filter Filter.instTop topologicalSpace Pi.topologicalSpace DFunLike.coe instDFunLike	—	isEmbedding_coe_of_principal Filter.principal_univ
isEmbedding_inclusion_principal 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.principal	Topology.IsEmbedding RestrictedProduct Filter.principal topologicalSpace inclusion	—	Topology.IsEmbedding.of_comp continuous_inclusion continuous_coe isEmbedding_coe_of_principal
isEmbedding_inclusion_top 📖	mathematical	—	Topology.IsEmbedding RestrictedProduct Top.top Filter OrderTop.toTop Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder CoheytingAlgebra.toOrderTop Order.Coframe.toCoheytingAlgebra Filter.instCoframe topologicalSpace inclusion le_top	—	Topology.IsEmbedding.of_comp le_top continuous_inclusion continuous_coe isEmbedding_coe_of_top
isEmbedding_structureMap 📖	mathematical	—	Topology.IsEmbedding RestrictedProduct Pi.topologicalSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership topologicalSpace structureMap	—	Topology.IsEmbedding.comp le_top isEmbedding_inclusion_top Homeomorph.isEmbedding
isOpenEmbedding_inclusion_principal 📖	mathematical	IsOpen Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.cofinite Filter.principal	Topology.IsOpenEmbedding RestrictedProduct Filter.principal Filter.cofinite topologicalSpace inclusion	—	isEmbedding_inclusion_principal range_inclusion isOpen_forall_imp_mem
isOpenEmbedding_structureMap 📖	mathematical	IsOpen	Topology.IsOpenEmbedding RestrictedProduct Filter.cofinite Pi.topologicalSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership topologicalSpace structureMap	—	isEmbedding_structureMap range_structureMap isOpen_forall_mem
isOpen_forall_imp_mem 📖	mathematical	IsOpen	IsOpen RestrictedProduct Filter.cofinite topologicalSpace setOf	—	topologicalSpace_eq_iSup isOpen_forall_imp_mem_of_principal
isOpen_forall_imp_mem_of_principal 📖	mathematical	IsOpen Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.cofinite Filter.principal	IsOpen RestrictedProduct Filter.principal topologicalSpace setOf	—	Set.ext IsOpen.preimage continuous_coe isOpen_set_pi Set.Finite.inter_of_left Filter.le_principal_iff
isOpen_forall_mem 📖	mathematical	IsOpen	IsOpen RestrictedProduct Filter.cofinite topologicalSpace setOf	—	topologicalSpace_eq_iSup isOpen_forall_mem_of_principal
isOpen_forall_mem_of_principal 📖	mathematical	IsOpen Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.cofinite Filter.principal	IsOpen RestrictedProduct Filter.principal topologicalSpace setOf	—	isOpen_forall_imp_mem_of_principal
isTopologicalAddGroup 📖	mathematical	AddSubgroupClass AddGroup.toSubNegMonoid IsTopologicalAddGroup	IsTopologicalAddGroup RestrictedProduct SetLike.coe Filter.cofinite topologicalSpace instAddGroupCoeOfAddSubgroupClass	—	instContinuousAddCoeCofinite IsTopologicalAddGroup.toContinuousAdd instContinuousNegCoe IsTopologicalAddGroup.toContinuousNeg
isTopologicalGroup 📖	mathematical	SubgroupClass Group.toDivInvMonoid IsTopologicalGroup	IsTopologicalGroup RestrictedProduct SetLike.coe Filter.cofinite topologicalSpace instGroupCoeOfSubgroupClass	—	instContinuousMulCoeCofinite IsTopologicalGroup.toContinuousMul instContinuousInvCoe IsTopologicalGroup.toContinuousInv
isTopologicalRing 📖	mathematical	SubringClass Ring.toNonAssocRing IsTopologicalRing NonAssocRing.toNonUnitalNonAssocRing	IsTopologicalRing RestrictedProduct SetLike.coe Filter.cofinite topologicalSpace NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCoeOfSubringClass	—	instContinuousAddCoeCofinite IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instContinuousMulCoeCofinite IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instContinuousNegCoe IsSemitopologicalRing.toContinuousNeg
locallyCompactSpace_of_addGroup 📖	mathematical	AddSubgroupClass AddGroup.toSubNegMonoid IsTopologicalAddGroup LocallyCompactSpace	LocallyCompactSpace RestrictedProduct SetLike.coe Filter.cofinite topologicalSpace	—	WeaklyLocallyCompactSpace.locallyCompactSpace instR1Space IsTopologicalAddGroup.regularSpace isTopologicalAddGroup weaklyLocallyCompactSpace_of_cofinite Fact.out instWeaklyLocallyCompactSpaceOfLocallyCompactSpace
locallyCompactSpace_of_group 📖	mathematical	SubgroupClass Group.toDivInvMonoid IsTopologicalGroup LocallyCompactSpace	LocallyCompactSpace RestrictedProduct SetLike.coe Filter.cofinite topologicalSpace	—	WeaklyLocallyCompactSpace.locallyCompactSpace instR1Space IsTopologicalGroup.regularSpace isTopologicalGroup weaklyLocallyCompactSpace_of_cofinite Fact.out instWeaklyLocallyCompactSpaceOfLocallyCompactSpace
mapAlong_continuous 📖	mathematical	Filter.Tendsto Filter.Eventually Set.MapsTo Continuous	Continuous RestrictedProduct topologicalSpace mapAlong	—	continuous_dom Filter.le_principal_iff Filter.inter_mem Continuous.comp continuous_inclusion continuous_rng_of_principal continuous_pi continuous_eval
nhds_eq_map_inclusion 📖	mathematical	IsOpen Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.cofinite Filter.principal	nhds RestrictedProduct Filter.cofinite topologicalSpace inclusion Filter.principal Filter.map	—	Topology.IsOpenEmbedding.map_nhds_eq isOpenEmbedding_inclusion_principal
nhds_eq_map_structureMap 📖	mathematical	IsOpen	nhds RestrictedProduct Filter.cofinite topologicalSpace structureMap Filter.map Pi.topologicalSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	Topology.IsOpenEmbedding.map_nhds_eq isOpenEmbedding_structureMap
nhds_zero_eq_map_ofPre 📖	mathematical	ZeroMemClass IsOpen SetLike.coe Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.cofinite Filter.principal	nhds RestrictedProduct Filter.cofinite topologicalSpace SetLike.coe inclusion Filter.principal instZeroCoeOfZeroMemClass Filter.map	—	nhds_eq_map_inclusion
nhds_zero_eq_map_structureMap 📖	mathematical	ZeroMemClass IsOpen SetLike.coe	nhds RestrictedProduct Filter.cofinite topologicalSpace SetLike.coe structureMap Pi.instZero Set.Elem ZeroMemClass.zero Filter.map Pi.topologicalSpace instTopologicalSpaceSubtype Set Set.instMembership	—	nhds_eq_map_structureMap
topologicalSpace_eq_iSup 📖	mathematical	—	topologicalSpace iSup TopologicalSpace RestrictedProduct Set ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.principal TopologicalSpace.coinduced inclusion	—	iSup_congr_Prop topologicalSpace_eq_of_principal
topologicalSpace_eq_of_bot 📖	mathematical	—	topologicalSpace Bot.bot Filter Filter.instBot TopologicalSpace.induced RestrictedProduct DFunLike.coe instDFunLike TopologicalSpace Pi.topologicalSpace	—	topologicalSpace_eq_of_principal Filter.principal_empty
topologicalSpace_eq_of_principal 📖	mathematical	—	topologicalSpace Filter.principal TopologicalSpace.induced RestrictedProduct DFunLike.coe instDFunLike TopologicalSpace Pi.topologicalSpace	—	le_antisymm continuous_iff_le_induced continuous_coe le_iSup₂_of_le le_rfl le_refl inclusion_eq_id coinduced_id
topologicalSpace_eq_of_top 📖	mathematical	—	topologicalSpace Top.top Filter Filter.instTop TopologicalSpace.induced RestrictedProduct DFunLike.coe instDFunLike TopologicalSpace Pi.topologicalSpace	—	topologicalSpace_eq_of_principal Filter.principal_univ
weaklyLocallyCompactSpace_of_cofinite 📖	mathematical	IsOpen WeaklyLocallyCompactSpace	WeaklyLocallyCompactSpace RestrictedProduct Filter.cofinite topologicalSpace	—	Filter.le_principal_iff Filter.Eventually.and exists_inclusion_eq_of_eventually nhds_eq_map_inclusion WeaklyLocallyCompactSpace.exists_compact_mem_nhds weaklyLocallyCompactSpace_of_principal IsCompact.image continuous_inclusion Filter.image_mem_map
weaklyLocallyCompactSpace_of_principal 📖	mathematical	WeaklyLocallyCompactSpace Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.cofinite Filter.principal IsCompact	WeaklyLocallyCompactSpace RestrictedProduct Filter.principal topologicalSpace	—	WeaklyLocallyCompactSpace.exists_compact_mem_nhds isCompact_univ_pi set_pi_mem_nhds Filter.mem_cofinite Filter.le_principal_iff Topology.IsInducing.isCompact_preimage_iff Topology.IsEmbedding.toIsInducing isEmbedding_coe_of_principal range_coe_principal Set.pi_if Set.inter_subset_left Filter.mem_of_superset Topology.IsInducing.nhds_eq_comap Filter.preimage_mem_comap

(root)

Definitions

Name	Category	Theorems
TopologicalSpace 📖	CompData	242 math math: continuousNeg_iInf, Topology.lawson_le_scott, coinduced_bot, continuous_sInf_dom₂, PolynormableSpace.sInf, continuous_sup_rng_right, GroupTopology.toTopologicalSpace_iInf, equicontinuousWithinAt_iInf_dom, continuousMul_inf, ContinuousMap.compactOpen_eq_iInf_induced, nhds_sInf, continuousMul_sInf, AddGroupTopology.toTopologicalSpace_inf, setOf_isOpen_iSup, isClosed_iSup_iff, topologicalGroup_iInf, PolishSpace.exists_polishSpace_forall_le, le_nhdsAdjoint_iff, continuous_sup_dom, TopologicalSpace.generatedBy_mono, Topology.IsGeneratedBy.le_generatedBy, R1Space.iInf, TopologicalSpace.setOf_isOpen_injective, nhds_iInf, UCompactlyGeneratedSpace.le_compactlyGenerated, continuous_sSup_dom, isClosed_sSup_iff, MeasureTheory.LevyProkhorov.eq_convergenceInDistribution, induced_inf, inseparable_top, GroupTopology.toTopologicalSpace_inf, TopologicalSpace.eq_induced_by_maps_to_sierpinski, LocallyConvexSpace.inf, deltaGenerated_eq_coinduced, continuousVAdd_sInf, deltaGenerated_le, le_of_nhds_le_nhds, MeasureTheory.analyticSet_iff_exists_polishSpace_range, generateFrom_sUnion, continuous_inf_dom_left₂, AddGroupTopology.toTopologicalSpace_injective, t2Space_antitone, induced_const, generateFrom_iUnion_isOpen, continuousAdd_inf, TopologicalSpace.eq_top_iff_forall_inseparable, continuous_inf_dom_right₂, UniformSpace.toTopologicalSpace_top, generateFrom_union, isOpen_sup, AddGroupTopology.toTopologicalSpace_sInf, UniformConvergenceCLM.topologicalSpace_mono, TopCat.pullback_topology, generateFrom_iInter_of_generateFrom_eq_self, TopCat.colimit_topology, topologicalGroup_inf, Pi.induced_restrict, Measurable.exists_continuous, Topology.upperSet_le_scott, topologicalAddGroup_inf, induced_topology_pure, continuousNeg_sInf, continuous_sSup_rng, continuousNeg_inf, TopCat.prod_topology, IndiscreteTopology.eq_top, regularSpace_sInf, topologicalAddGroup_sInf, TopologicalSpace.isOpen_top_iff, TopologicalSpace.IsTopologicalBasis.inf_induced, continuous_iInf_rng, TopologicalSpace.le_def, Topology.IsGeneratedBy.iff_le_generatedBy, continuous_bot, continuousInv_inf, TopologicalSpace.generateFrom_surjective, continuous_inf_dom_right, TopologicalSpace.generateFrom_anti, isOpen_sSup_iff, isDenseEmbedding_pure, induced_sInf, Topology.isLawson_le_isScott, le_nhdsAdjoint_iff', TopCat.nonempty_isLimit_iff_eq_induced, SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf, CompletePseudometrizable.iInf, SequentialSpace.iSup, continuousInv_sInf, RingTopology.toTopologicalSpace_injective, continuous_top, pullbackTopology_def, le_induced_generateFrom, TopologicalSpace.secondCountableTopology_iInf, AddGroupTopology.toTopologicalSpace_top, LocallyConvexSpace.iInf, Topology.IsGeneratedBy.sup, Topology.scottHausdorff_le_isLawson, t1Space_antitone, continuousSMul_sInf, DeltaGeneratedSpace.le_deltaGenerated, generateFrom_iUnion, PolynormableSpace.induced, coinduced_sSup, LinearMap.mem_span_iff_continuous_of_finite, nhds_top, Topology.scottHausdorff_le_lawson, UniformOnFun.topologicalSpace_eq, TopologicalSpace.IsTopologicalBasis.inf, GroupTopology.toTopologicalSpace_sInf, continuousAdd_iInf, Continuous.homeoOfEquivCompactToT2.t1_counterexample, regularSpace_iInf, continuous_iSup_dom, R1Space.inf, equicontinuous_iInf_dom, UniformSpace.toTopologicalSpace_bot, CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap_hom, generateFrom_iInter, alexandrovDiscrete_iSup, continuous_iff_le_induced, coinduced_le_iff_le_induced, continuous_sInf_dom, exists_opensMeasurableSpace_of_countablySeparated, RestrictedProduct.topologicalSpace_eq_of_principal, UniformSpace.toTopologicalSpace_sInf, GroupTopology.toTopologicalSpace_bot, PolynormableSpace.iInf, nhds_inf, TopCat.coinduced_of_isColimit, topologicalGroup_sInf, isOpen_iSup_iff, Topology.IsScott.scottHausdorff_le, ModuleTopology.eq_coinduced_of_surjectiveₛₗ, Topology.scottHausdorff_le_scott, AlexandrovDiscrete.sup, AddGroupTopology.toTopologicalSpace_le, ModuleTopology.eq_coinduced_of_surjective, Pi.induced_precomp, UniformSpace.toTopologicalSpace_iInf, indiscreteTopology_iff, Topology.scottHausdorff_le_lower, continuousSMul_inf, continuousAdd_sInf, DeltaGeneratedSpace.sup, continuous_id_iff_le, LocallyConvexSpace.sInf, RegularSpace.inf, Units.topology_eq_inf, induced_topology_le_preorder, completelyRegularSpace_iInf, continuousSMul_iInf, coinduced_iSup, IsTopologicalBasis.iInf, le_iff_nhds, Pi.induced_restrict_sUnion, discreteTopology_bot, equicontinuousAt_iInf_dom, completelyRegularSpace_inf, isDenseInducing_pure, Continuous.le_induced, continuous_iSup_rng, StandardBorelSpace.polish, NormedSpace.Dual.dual_norm_topology_le_weak_dual_topology, TopologicalSpace.prod_mono, TopologicalSpace.generatedBy_le, induced_to_pi, continuousMul_iInf, moduleTopology_le, TopCat.induced_of_isLimit, deltaGenerated_mono, isOpen_implies_isOpen_iff, continuous_iInf_dom, TopologicalSpace.gc_generateFrom, continuousVAdd_inf, coinduced_sup, LinearOrder.bot_topologicalSpace_eq_generateFrom, inducing_iInf_to_pi, TopCat.nonempty_isColimit_iff_eq_coinduced, DiscreteTopology.eq_bot, GroupTopology.toTopologicalSpace_le, equicontinuousOn_iInf_dom, gc_nhds, generateFrom_union_isOpen, MeasurableSet.isClopenable', RestrictedProduct.topologicalSpace_eq_of_bot, UniformSpace.toTopologicalSpace_inf, eq_bot_of_singletons_open, Topology.IsUpperSet.upperSet_le_upper, induced_mono, MeasureTheory.LevyProkhorov.le_convergenceInDistribution, Pi.induced_precomp', MvPowerSeries.WithPiTopology.instTopologicalSpace_mono, continuous_iff_coinduced_le, continuousInv_iInf, MeasureTheory.levyProkhorov_le_convergenceInDistribution, Topology.lawson_le_lower, borel_anti, RestrictedProduct.topologicalSpace_eq_iSup, withSeminorms_iInf, ContinuousMap.compactOpen_le_induced, continuous_sup_rng_left, induced_top, UniformSpace.toTopologicalSpace_mono, setOf_isOpen_sSup, Topology.IsLower.scottHausdorff_le, continuous_inf_rng, RestrictedProduct.topologicalSpace_eq_of_top, GroupTopology.toTopologicalSpace_top, AddGroupTopology.toTopologicalSpace_iInf, Topology.IsGeneratedBy.iSup, PolishSpace.iInf, induced_iInf, TopCat.limit_topology, exists_borelSpace_of_countablyGenerated_of_separatesPoints, generateFrom_inter, TestFunction.topologicalSpace_le_iff, R1Space.sInf, PolynormableSpace.inf, coinduced_mono, TopologicalSpace.leftInverse_generateFrom, SequentialSpace.sup, instIndiscreteTopology, LinearMap.mem_span_iff_continuous, AddUnits.topology_eq_inf, topologicalAddGroup_iInf, Topology.IsLowerSet.lowerSet_le_lower, DeltaGeneratedSpace.iSup, gc_coinduced_induced, continuous_inf_dom_left, GroupTopology.toTopologicalSpace_injective, continuous_sInf_rng, TopologicalSpace.le_generateFrom_iff_subset_isOpen, le_generateFrom, TopologicalSpace.Opens.IsBasis.le_iff, TestFunction.originalTop_le, Continuous.coinduced_le, continuousVAdd_iInf, IsTopologicalBasis.iInf_induced, LinearMap.withSeminorms_induced, AddGroupTopology.toTopologicalSpace_bot, setOf_isOpen_sup, MeasureTheory.levyProkhorov_eq_convergenceInDistribution

---

← Back to Index