Constructions

📁 Source: Mathlib/Topology/Constructions.lean

Statistics

Metric	Count
Definitions CofiniteTopology, instInhabited, instTopologicalSpace, of, ofEqSubtypes, piCurry, IsDiscrete, instTopologicalSpace, topologicalSpace, topologicalSpace, instTopologicalSpaceAdditive, instTopologicalSpaceMultiplicative, instTopologicalSpaceQuot, instTopologicalSpaceQuotient, instTopologicalSpaceSigma	15
Theorems isClosed_iff, isOpen_iff, isOpen_iff', mem_nhds_iff, nhds_eq, codRestrict, finCons, finInit, finInsertNth, finSnoc, finTail, matrixVecCons, piMap, quotient_lift, quotient_liftOn', quotient_map', rangeFactorization, restrict, restrictPreimage, sigma_map, subtype_coind, subtype_map, subtype_mk, subtype_val, update, codRestrict, finCons, finInit, finInsertNth, finSnoc, finTail, matrixVecCons, piMap, restrict, restrictPreimage, update, quotient, quotient, isDiscrete, of_subset, preimage_of_continuous_injective, prod_nhdsSet, apply_nhds, finCons, finInit, finInsertNth, finSnoc, finTail, matrixVecCons, update, eventually_nhdsSet_prod_iff, continuous_restrict, continuous_restrict_apply, continuous_restrict₂, continuous_restrict₂_apply, isEmbedding_comp, ofEqSubtypes_toEquiv, piCurry_apply, piCurry_symm_apply, inter_preimage_val_iff, isClosedEmbedding_subtypeVal, isClosedMap_inclusion, isClosedMap_subtype_val, preimage_val, trans, codRestrict, mapsToRestrict, restrict, subtype_coind, subtype_map, subtype_mk, mono, to_subtype, inter_preimage_val_iff, isOpenEmbedding_subtypeVal, isOpenMap_inclusion, isOpenMap_subtype_val, preimage_val, trans, codRestrict, mapsToRestrict, piMap, restrict, subtype_coind, subtype_map, subtype_mk, piMap, curry_prodMap, prodMap, instDiscreteTopology, instNeBotNhdsWithinIio, instNeBotNhdsWithinIoi, continuous_postcomp, continuous_postcomp', continuous_precomp, continuous_precomp', continuous_restrict, continuous_restrict_apply, continuous_restrict₂, continuous_restrict₂_apply, discreteTopology, induced_precomp, induced_precomp', induced_restrict, induced_restrict_sUnion, preimage_mem_nhds, isDiscrete_iff_discreteTopology, discreteTopology, nhds_eq, nhds_mk, dense_iff, discreteTopology, inclusion, piMap, sigmaMk, subtypeVal, uliftDown, codRestrict, inclusion, piMap, restrict, sigmaMk, subtypeVal, uliftDown, codRestrict, of_codRestrict, piMap, subtypeVal, inclusion, piMap, restrict, sigmaMk, restrictPreimage_isOpen, isEmbedding_sigmaMap, isInducing_sigmaMap, isOpenEmbedding_sigmaMap, isClosed_iff, isOpen_iff, closure_subtype, comap_nhdsWithin_range, comap_sigmaMk_nhds, continuousAt_apply, continuousAt_codRestrict_iff, continuousAt_pi, continuousAt_pi', continuousAt_subtype_val, continuous_apply, continuous_apply_apply, continuous_bool_rng, continuous_inclusion, continuous_map_of_le, continuous_map_sInf, continuous_mulSingle, continuous_ofAdd, continuous_ofDual, continuous_ofMul, continuous_pi, continuous_pi_iff, continuous_quot_lift, continuous_quot_mk, continuous_quotient_mk', continuous_rangeFactorization_iff, continuous_sigma, continuous_sigmaMk, continuous_sigma_iff, continuous_sigma_map, continuous_single, continuous_subtype_val, continuous_toAdd, continuous_toDual, continuous_toMul, continuous_uliftDown, continuous_uliftMap, continuous_uliftUp, continuous_update, denseRange_inclusion_iff, exists_finset_piecewise_mem_of_mem_nhds, exists_open_dense_of_open_dense_subtype, frontier_inter_open_inter, induced_to_pi, inducing_iInf_to_pi, inducing_sigma, instCompactSpaceAdditive, instCompactSpaceMultiplicative, instDiscreteTopologyAdditive, instDiscreteTopologyMultiplicative, instDiscreteTopologySubtype, instDiscreteTopologyULift, instLocallyCompactSpaceAdditive, instLocallyCompactSpaceMultiplicative, instNoncompactSpaceAdditive, instNoncompactSpaceMultiplicative, instWeaklyLocallyCompactSpaceAdditive, instWeaklyLocallyCompactSpaceMultiplicative, interior_pi_set, isClosedMap_ofAdd, isClosedMap_ofDual, isClosedMap_ofMul, isClosedMap_sigmaMk, isClosedMap_toAdd, isClosedMap_toDual, isClosedMap_toMul, isClosed_preimage_val, isClosed_range_sigmaMk, isClosed_set_pi, isClosed_sigma_iff, isDiscrete_iff_discreteTopology, isOpenMap_ofAdd, isOpenMap_ofDual, isOpenMap_ofMul, isOpenMap_sigma, isOpenMap_sigmaMk, isOpenMap_sigma_map, isOpenMap_toAdd, isOpenMap_toDual, isOpenMap_toMul, isOpen_pi_iff, isOpen_pi_iff', isOpen_range_sigmaMk, isOpen_set_pi, isOpen_sigma_fst_preimage, isOpen_sigma_iff, isQuotientMap_quot_mk, isQuotientMap_quotient_mk', map_nhds_subtype_coe_eq_nhds, map_nhds_subtype_val, mem_nhds_of_pi_mem_nhds, mem_nhds_subtype, nhdsSet_prod_le, nhdsWithin_subtype_eq_bot_iff, nhds_ne_subtype_eq_bot_iff, nhds_ne_subtype_neBot_iff, nhds_ofAdd, nhds_ofDual, nhds_ofMul, nhds_pi, nhds_subtype, nhds_subtype_eq_comap, nhds_subtype_eq_comap_nhdsWithin, nhds_toAdd, nhds_toDual, nhds_toMul, pi_eq_generateFrom, pi_generateFrom_eq, pi_generateFrom_eq_finite, set_pi_mem_nhds, set_pi_mem_nhds_iff, tendsto_pi_nhds, tendsto_subtype_rng	249
Total	264

CofiniteTopology

Definitions

Name	Category	Theorems
instInhabited 📖	CompOp	—
instTopologicalSpace 📖	CompOp	12 math math: instT1SpaceCofiniteTopology, continuous_of, mem_nhds_iff, nhds_eq, TopologicalSpace.instNoetherianSpaceCofiniteTopology, t1Space_TFAE, isClosed_iff, instIrreducibleSpaceCofiniteTopologyOfInfinite, t1Space_iff_continuous_cofinite_of, OnePoint.not_continuous_cofiniteTopology_of_symm, isOpen_iff, isOpen_iff'
of 📖	CompOp	4 math math: continuous_of, t1Space_TFAE, t1Space_iff_continuous_cofinite_of, OnePoint.not_continuous_cofiniteTopology_of_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed_iff 📖	mathematical	—	IsClosed CofiniteTopology instTopologicalSpace Set.univ Set.Finite	—	compl_compl
isOpen_iff 📖	mathematical	—	IsOpen CofiniteTopology instTopologicalSpace Set.Finite Compl.compl Set Set.instCompl	—	—
isOpen_iff' 📖	mathematical	—	IsOpen CofiniteTopology instTopologicalSpace Set Set.instEmptyCollection Set.Finite Compl.compl Set.instCompl	—	—
mem_nhds_iff 📖	mathematical	—	Set CofiniteTopology Filter Filter.instMembership nhds instTopologicalSpace Set.instMembership Set.Finite Compl.compl Set.instCompl	—	nhds_eq
nhds_eq 📖	mathematical	—	nhds CofiniteTopology instTopologicalSpace Filter Filter.instSup Filter.instPure Filter.cofinite	—	Filter.ext mem_nhds_iff Filter.mem_sup Filter.mem_of_superset Set.Subset.rfl

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codRestrict 📖	mathematical	Continuous Set Set.instMembership	Set.Elem instTopologicalSpaceSubtype Set.codRestrict	—	—
finCons 📖	mathematical	Continuous Pi.topologicalSpace	Fin.cons	—	continuous_iff_continuousAt ContinuousAt.finCons continuousAt
finInit 📖	mathematical	Continuous Pi.topologicalSpace	Fin.init	—	continuous_iff_continuousAt ContinuousAt.finInit continuousAt
finInsertNth 📖	mathematical	Continuous Pi.topologicalSpace Fin.succAbove	Fin.insertNth	—	continuous_iff_continuousAt ContinuousAt.finInsertNth continuousAt
finSnoc 📖	mathematical	Continuous Pi.topologicalSpace	Fin.snoc	—	continuous_iff_continuousAt ContinuousAt.finSnoc continuousAt
finTail 📖	mathematical	Continuous Pi.topologicalSpace	Fin.tail	—	continuous_iff_continuousAt ContinuousAt.finTail continuousAt
matrixVecCons 📖	mathematical	Continuous Pi.topologicalSpace	Matrix.vecCons	—	finCons
piMap 📖	mathematical	Continuous	Pi.topologicalSpace Pi.map	—	continuous_pi comp continuous_apply
quotient_lift 📖	mathematical	Continuous	instTopologicalSpaceQuotient	—	continuous_coinduced_dom
quotient_liftOn' 📖	mathematical	Continuous	instTopologicalSpaceQuotient Quotient.liftOn'	—	quotient_lift
quotient_map' 📖	mathematical	Continuous Relator.LiftFun	instTopologicalSpaceQuotient Quotient.map'	—	quotient_lift comp continuous_quotient_mk'
rangeFactorization 📖	mathematical	Continuous	Set.Elem Set.range instTopologicalSpaceSubtype Set Set.instMembership Set.rangeFactorization	—	continuous_rangeFactorization_iff
restrict 📖	mathematical	Set.MapsTo Continuous	Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.MapsTo.restrict	—	codRestrict comp continuous_subtype_val
restrictPreimage 📖	mathematical	Continuous	Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	restrict Set.mapsTo_preimage
sigma_map 📖	mathematical	Continuous	instTopologicalSpaceSigma Sigma.map	—	continuous_sigma_map
subtype_coind 📖	mathematical	Continuous	instTopologicalSpaceSubtype Subtype.coind	—	—
subtype_map 📖	mathematical	Continuous	instTopologicalSpaceSubtype Subtype.map	—	comp continuous_subtype_val
subtype_mk 📖	mathematical	Continuous	instTopologicalSpaceSubtype	—	continuous_induced_rng
subtype_val 📖	—	Continuous instTopologicalSpaceSubtype	—	—	comp continuous_subtype_val
update 📖	mathematical	Continuous Pi.topologicalSpace	Function.update	—	continuous_iff_continuousAt ContinuousAt.update continuousAt

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codRestrict 📖	mathematical	Set Set.instMembership ContinuousAt	Set.Elem instTopologicalSpaceSubtype Set.codRestrict	—	continuousAt_codRestrict_iff
finCons 📖	mathematical	ContinuousAt Pi.topologicalSpace	Fin.cons	—	Filter.Tendsto.finCons tendsto
finInit 📖	mathematical	ContinuousAt Pi.topologicalSpace	Fin.init	—	Filter.Tendsto.finInit tendsto
finInsertNth 📖	mathematical	ContinuousAt Pi.topologicalSpace Fin.succAbove	Fin.insertNth	—	Filter.Tendsto.finInsertNth tendsto
finSnoc 📖	mathematical	ContinuousAt Pi.topologicalSpace	Fin.snoc	—	Filter.Tendsto.finSnoc tendsto
finTail 📖	mathematical	ContinuousAt Pi.topologicalSpace	Fin.tail	—	Filter.Tendsto.finTail tendsto
matrixVecCons 📖	mathematical	ContinuousAt Pi.topologicalSpace	Matrix.vecCons	—	finCons
piMap 📖	mathematical	ContinuousAt	Pi.topologicalSpace Pi.map	—	continuousAt_pi comp continuousAt_apply
restrict 📖	mathematical	Set.MapsTo ContinuousAt Set Set.instMembership	Set.Elem instTopologicalSpaceSubtype Set.MapsTo.restrict	—	codRestrict comp continuousAt_subtype_val
restrictPreimage 📖	mathematical	ContinuousAt Set Set.instMembership Set.preimage	Set.Elem instTopologicalSpaceSubtype Set.restrictPreimage	—	restrict Set.mapsTo_preimage
update 📖	mathematical	ContinuousAt Pi.topologicalSpace	Function.update	—	Filter.Tendsto.update tendsto

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quotient 📖	mathematical	Dense	instTopologicalSpaceQuotient Set.image	—	DenseRange.dense_image Function.Surjective.denseRange Quotient.mk''_surjective continuous_coinduced_rng

DenseRange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quotient 📖	mathematical	DenseRange	instTopologicalSpaceQuotient	—	comp Function.Surjective.denseRange Quotient.mk''_surjective continuous_coinduced_rng

DiscreteTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDiscrete 📖	mathematical	—	IsDiscrete	—	—
of_subset 📖	mathematical	Set Set.instHasSubset	DiscreteTopology Set.Elem instTopologicalSpaceSubtype Set.instMembership	—	Topology.IsEmbedding.discreteTopology Topology.IsEmbedding.inclusion
preimage_of_continuous_injective 📖	mathematical	Continuous	DiscreteTopology Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership	—	of_continuous_injective Continuous.restrict Function.Injective.injOn

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_nhdsSet_prod_iff 📖	mathematical	—	Eventually nhdsSet instTopologicalSpaceProd SProd.sprod Set Set.instSProd nhds	—	nhds_prod_eq

Filter.Eventually

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_nhdsSet 📖	mathematical	Filter.Eventually nhdsSet	instTopologicalSpaceProd SProd.sprod Set Set.instSProd	—	nhdsSet_prod_le Filter.mem_of_superset Filter.prod_mem_prod

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_nhds 📖	—	Filter.Tendsto nhds Pi.topologicalSpace	—	—	comp ContinuousAt.tendsto continuousAt_apply
finCons 📖	mathematical	Filter.Tendsto nhds Pi.topologicalSpace	Fin.cons	—	tendsto_pi_nhds Fin.cons_zero Fin.cons_succ
finInit 📖	mathematical	Filter.Tendsto nhds Pi.topologicalSpace	Fin.init	—	tendsto_pi_nhds apply_nhds
finInsertNth 📖	mathematical	Filter.Tendsto nhds Pi.topologicalSpace Fin.succAbove	Fin.insertNth	—	tendsto_pi_nhds Fin.insertNth_apply_same Fin.insertNth_apply_succAbove
finSnoc 📖	mathematical	Filter.Tendsto nhds Pi.topologicalSpace	Fin.snoc	—	tendsto_pi_nhds Fin.snoc_last Fin.snoc_castSucc
finTail 📖	mathematical	Filter.Tendsto nhds Pi.topologicalSpace	Fin.tail	—	tendsto_pi_nhds apply_nhds
matrixVecCons 📖	mathematical	Filter.Tendsto nhds Pi.topologicalSpace	Matrix.vecCons	—	finCons
update 📖	mathematical	Filter.Tendsto nhds Pi.topologicalSpace	Function.update	—	tendsto_pi_nhds eq_or_ne Function.update_self Function.update_of_ne apply_nhds

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_restrict 📖	mathematical	—	Continuous Pi.topologicalSpace Finset SetLike.instMembership instSetLike restrict	—	continuous_pi continuous_apply
continuous_restrict_apply 📖	mathematical	Continuous	Finset SetLike.instMembership instSetLike instTopologicalSpaceSubtype restrict	—	Continuous.comp continuous_subtype_val
continuous_restrict₂ 📖	mathematical	Finset instHasSubset	Continuous Pi.topologicalSpace SetLike.instMembership instSetLike restrict₂	—	continuous_pi continuous_apply
continuous_restrict₂_apply 📖	mathematical	Finset instHasSubset Continuous SetLike.instMembership instSetLike instTopologicalSpaceSubtype	restrict₂	—	Continuous.comp continuous_inclusion

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isEmbedding_comp 📖	mathematical	—	Topology.IsEmbedding Pi.topologicalSpace	—	Topology.isInducing_iff_nhds nhds_pi iInf_congr Filter.comap_iInf Filter.comap_comap injective_comp_right

Homeomorph

Definitions

Name	Category	Theorems
ofEqSubtypes 📖	CompOp	1 math math: ofEqSubtypes_toEquiv
piCurry 📖	CompOp	2 math math: piCurry_apply, piCurry_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofEqSubtypes_toEquiv 📖	mathematical	—	toEquiv instTopologicalSpaceSubtype ofEqSubtypes Equiv.subtypeEquivProp	—	—
piCurry_apply 📖	mathematical	—	DFunLike.coe Homeomorph Pi.topologicalSpace EquivLike.toFunLike instEquivLike piCurry	—	—
piCurry_symm_apply 📖	mathematical	—	DFunLike.coe Homeomorph Pi.topologicalSpace EquivLike.toFunLike instEquivLike symm piCurry	—	—

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inter_preimage_val_iff 📖	mathematical	—	IsClosed Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.preimage Set.instInter	—	Subtype.image_preimage_coe isClosedMap_subtype_val preimage_val Subtype.preimage_coe_self_inter
isClosedEmbedding_subtypeVal 📖	mathematical	—	Topology.IsClosedEmbedding Set Set.instMembership instTopologicalSpaceSubtype	—	Topology.IsClosedEmbedding.subtypeVal
isClosedMap_inclusion 📖	mathematical	Set Set.instHasSubset	IsClosedMap Set.Elem instTopologicalSpaceSubtype Set.instMembership Set.inclusion	—	IsClosedMap.subtype_map IsClosedMap.id
isClosedMap_subtype_val 📖	mathematical	—	IsClosedMap Set Set.instMembership instTopologicalSpaceSubtype	—	Topology.IsClosedEmbedding.isClosedMap isClosedEmbedding_subtypeVal
preimage_val 📖	mathematical	—	IsClosed Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.preimage	—	preimage continuous_subtype_val
trans 📖	mathematical	—	IsClosed Set.image Set Set.instMembership	—	isClosed_induced_iff Subtype.image_preimage_coe inter

IsClosedMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codRestrict 📖	mathematical	IsClosedMap Set Set.instMembership	Set.Elem instTopologicalSpaceSubtype Set.codRestrict	—	—
mapsToRestrict 📖	mathematical	IsClosedMap Set.MapsTo	Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.MapsTo.restrict	—	codRestrict restrict
restrict 📖	mathematical	IsClosedMap	Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.restrict	—	comp IsClosed.isClosedMap_subtype_val
subtype_coind 📖	mathematical	IsClosedMap	instTopologicalSpaceSubtype Subtype.coind	—	—
subtype_map 📖	mathematical	IsClosedMap Set Set.instMembership	instTopologicalSpaceSubtype Subtype.map	—	comp IsClosed.isClosedMap_subtype_val
subtype_mk 📖	mathematical	IsClosedMap	instTopologicalSpaceSubtype	—	Set.ext IsClosed.preimage continuous_subtype_val

IsDiscrete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	IsDiscrete Set Set.instHasSubset	—	—	DiscreteTopology.of_subset to_subtype
to_subtype 📖	mathematical	IsDiscrete	DiscreteTopology Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	—

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inter_preimage_val_iff 📖	mathematical	IsOpen	Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.preimage Set.instInter	—	Subtype.image_preimage_coe isOpenMap_subtype_val preimage_val Subtype.preimage_coe_self_inter
isOpenEmbedding_subtypeVal 📖	mathematical	IsOpen	Topology.IsOpenEmbedding Set Set.instMembership instTopologicalSpaceSubtype	—	Topology.IsEmbedding.subtypeVal Subtype.range_coe
isOpenMap_inclusion 📖	mathematical	IsOpen Set Set.instHasSubset	IsOpenMap Set.Elem instTopologicalSpaceSubtype Set.instMembership Set.inclusion	—	IsOpenMap.subtype_map IsOpenMap.id
isOpenMap_subtype_val 📖	mathematical	IsOpen	IsOpenMap Set Set.instMembership instTopologicalSpaceSubtype	—	Topology.IsOpenEmbedding.isOpenMap isOpenEmbedding_subtypeVal
preimage_val 📖	mathematical	IsOpen	Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.preimage	—	preimage continuous_subtype_val
trans 📖	mathematical	IsOpen Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	Set.image	—	isOpen_induced_iff Subtype.image_preimage_coe inter

IsOpenMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codRestrict 📖	mathematical	IsOpenMap Set Set.instMembership	Set.Elem instTopologicalSpaceSubtype Set.codRestrict	—	—
mapsToRestrict 📖	mathematical	IsOpenMap IsOpen Set.MapsTo	Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.MapsTo.restrict	—	codRestrict restrict
piMap 📖	mathematical	IsOpenMap	Pi.topologicalSpace Pi.map	—	of_nhds_le nhds_pi Filter.map_piMap_pi Filter.pi_mono nhds_le
restrict 📖	mathematical	IsOpenMap IsOpen	Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.restrict	—	comp IsOpen.isOpenMap_subtype_val
subtype_coind 📖	mathematical	IsOpenMap	instTopologicalSpaceSubtype Subtype.coind	—	—
subtype_map 📖	mathematical	IsOpenMap IsOpen Set Set.instMembership	instTopologicalSpaceSubtype Subtype.map	—	comp IsOpen.isOpenMap_subtype_val
subtype_mk 📖	mathematical	IsOpenMap	instTopologicalSpaceSubtype	—	Set.ext IsOpen.preimage continuous_subtype_val

IsOpenQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
piMap 📖	mathematical	IsOpenQuotientMap	Pi.topologicalSpace Pi.map	—	Function.Surjective.piMap surjective Continuous.piMap continuous IsOpenMap.piMap isOpenMap Filter.Eventually.of_forall

MapClusterPt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
curry_prodMap 📖	mathematical	—	MapClusterPt instTopologicalSpaceProd Filter.curry	—	Filter.HasBasis.mapClusterPt_iff_frequently Filter.HasBasis.prod_nhds Filter.basis_sets Filter.frequently_curry_iff Filter.Frequently.mono mapClusterPt_iff_frequently
prodMap 📖	mathematical	—	MapClusterPt instTopologicalSpaceProd SProd.sprod Filter Filter.instSProd	—	mono curry_prodMap Filter.map_mono Filter.curry_le_prod

OrderDual

Definitions

Name	Category	Theorems
instTopologicalSpace 📖	CompOp	46 math math: Topology.isUpper_orderDual, instIsTopologicalGroup, instNeBotNhdsWithinIio, instIsUpper, instSeparableSpaceOrderDual, borelSpace, supConvergenceClass, instFirstCountableTopologyOrderDual, instIsLower, instCompactIccSpaceOrderDual, instContinuousAddOrderDual, instIsLowerSet, continuous_ofDual, Topology.isUpperSet_orderDual, instClosedIciTopologyOrderDual, isClosedMap_toDual, instBoundedGENhdsClassOrderDual, instContinuousNeg, isClosedMap_ofDual, instBoundedLENhdsClassOrderDual, topologicalLattice, instContinuousInv, instIsTopologicalAddGroup, instContinuousConstVAddOrderDual, continuous_toDual, nhds_ofDual, isOpenMap_ofDual, opensMeasurableSpace, infConvergenceClass, instNeBotNhdsWithinIoi, instIsUpperSet, instDiscreteTopology, instOrderClosedTopologyOrderDual, instOrderTopologyOrderDual, Topology.isLowerSet_orderDual, continuousInf, instContinuousMulOrderDual, Topology.isLower_orderDual, instHasUpperLowerClosureOrderDual, nhds_toDual, Dense.orderDual, continuousSup, instContinuousConstSMulOrderDual, isOpenMap_toDual, instSecondCountableTopologyOrderDual, instClosedIicTopologyOrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDiscreteTopology 📖	mathematical	—	DiscreteTopology OrderDual instTopologicalSpace	—	—
instNeBotNhdsWithinIio 📖	mathematical	—	Filter.NeBot OrderDual nhdsWithin instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toDual Set.Iio instPreorder	—	—
instNeBotNhdsWithinIoi 📖	mathematical	—	Filter.NeBot OrderDual nhdsWithin instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toDual Set.Ioi instPreorder	—	—

Pi

Definitions

Name	Category	Theorems
topologicalSpace 📖	CompOp	928 math math: pi_Iio_mem_nhds, comul_eq_adjoint, IsProperMap.pi_map, NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply', ContinuousLinearMap.sum_comp_single, PiLp.continuousLinearEquiv_symm_apply, continuousInv, hasStrictFDerivAt_apply, differentiableWithinAt_finCons', Filter.coprodᵢ_cocompact, Equicontinuous.inducing_uniformFun_iff_pi, isCompact_stdSimplex, Path.Homotopic.comp_pi_eq_pi_comp, NumberField.mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace, CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_snd, Homeomorph.finTwoArrow_apply, NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm, Continuous.matrix_blockDiag, NumberField.mixedEmbedding.fundamentalCone.interior_paramSet, NumberField.mixedEmbedding.measurable_polarCoordReal_symm, ContinuousMap.constPi_apply, isOpen_pi_iff, hasStrictFDerivAt_list_prod_finRange', ContinuousMultilinearMap.norm_iteratedFDerivComponent_le, NormedSpace.Dual.isClosed_image_polar_of_mem_nhds, Profinite.NobelingProof.injective_πs', FundamentalGroupoidFunctor.piIso_hom, Homeomorph.piCongr_apply, hasFDerivAtFilter_pi, Homeomorph.finTwoArrow_symm_apply, hasFDerivAt_multiset_prod, AlternatingMap.continuous_of_bound, WeakBilin.isEmbedding, hasProd, Matrix.l2_opNorm_mulVec, thickenedIndicatorAux_tendsto_indicator_closure, GenLoop.fromLoop_apply, differentiableWithinAt_pi'', EquicontinuousOn.tendsto_uniformOnFun_iff_pi', ContinuousMap.toEquiv_homeoFnOfDiscrete, Set.UniformEquicontinuousOn.closure, WeakDual.isClosed_image_polar_of_mem_nhds, RestrictedProduct.continuous_rng_of_principal, stdSimplexHomeomorphUnitInterval_symm_apply_coe, isOpenMap_eval, t2Space, Profinite.NobelingProof.Products.span_nil_eq_top, ContinuousAlternatingMap.opNNNorm_pi, Function.compactSpace, PiNat.exists_retraction_subtype_of_isClosed, Topology.RelCWComplex.continuousOn_symm, has_continuous_neg', EquicontinuousOn.isClosed_range_pi_of_uniformOnFun, Topology.CWComplex.continuousOn, NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isComplex, NumberField.mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_union_smaller, Profinite.NobelingProof.coe_πs, HomotopyGroup.symmAt_indep, pi_Ioo_mem_nhds, deltaGenerated_eq_coinduced, Bornology.isVonNBounded_pi_iff, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, differentiableOn_pi, RestrictedProduct.continuous_coe, Function.locallyCompactSpace, Path.pi_coe, isClosed_setOf_lipschitzOnWith, locallyConvexSpace, ContinuousMap.specializes_coe, ContinuousAlternatingMap.piLIE_apply_apply, instTietzeExtension, MeasureTheory.Integrable.of_eval, pi_Ico_mem_nhds', Profinite.NobelingProof.instSubsingletonLocallyConstantElemForallBoolEmptyCollectionSetInt, UnitAddTorus.mFourierSubalgebra_coe, Homeomorph.piCongrLeft_symm_apply, Matrix.blockDiagonal_tsum, ContinuousMultilinearMap.piLinearEquiv_symm_apply, ContinuousAlternatingMap.coe_pi, instIsTopologicalSemiring, pi_Iic_mem_nhds', NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume, continuous_equivFun_basis, ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image, NumberField.mixedEmbedding.fundamentalCone.compactSet_eq_union_aux₁, UnitAddTorus.mFourierSubalgebra_closure_eq_top, continuousAt_pi', HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, NumberField.mixedEmbedding.polarCoordReal_apply, instConnectedSpaceForall, Homeomorph.funSplitAt_symm_apply, Profinite.NobelingProof.Products.max_eq_eval, Homeomorph.toEquiv_piCongr, cfcₙ_map_pi, isClosed_setOf_map_add, continuous_precomp, hasDerivWithinAt_pi, Profinite.NobelingProof.Products.eval_πs, Homeomorph.toEquiv_piCongrLeft, ContinuousLinearMap.single_apply, Homeomorph.piCurry_apply, orderClosedTopology', Profinite.NobelingProof.GoodProducts.injective, MeasureTheory.ProbabilityMeasure.continuous_pi, stdSimplexHomeomorphUnitInterval_zero, IsClosed.lowerClosure_pi, Summable.matrix_blockDiag, GenLoop.homotopyTo_apply, differentiable_finCons', Fin.appendHomeomorph_apply, Function.update_exp, PiNat.isTopologicalBasis_cylinders, Homeomorph.sumArrowHomeomorphProdArrow_apply, hasStrictFDerivAt_pi', HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, LocallyConstant.eval_apply, PiLp.coe_continuousLinearEquiv, ContinuousMultilinearMap.linearDeriv_apply, NumberField.mixedEmbedding.polarSpaceCoord_target, NumberField.mixedEmbedding.negAt_apply_snd, EquicontinuousOn.tendsto_uniformOnFun_iff_pi, ContinuousAlternatingMap.piEquiv_apply, hasFDerivWithinAt_pi', ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, ContinuousMap.piEquiv_symm_apply, fderivWithin_pi, RestrictedProduct.isOpenEmbedding_structureMap, HomotopyGroup.isUnital_auxGroup, UniformOnFun.isEmbedding_toFun_finite, Profinite.NobelingProof.GoodProducts.equiv_toFun_eq_eval, Fin.consEquivL_apply, Topology.RelCWComplex.continuousOn, NumberField.mixedEmbedding.fundamentalCone.expMap_target, Filter.Tendsto.coeFun, NumberField.mixedEmbedding.negAt_preimage, NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne, MeasureTheory.charFunDual_pi', differentiable_apply, NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, Profinite.NobelingProof.Products.eval_πs', Profinite.NobelingProof.GoodProducts.span_sum, Profinite.NobelingProof.GoodProducts.range_equiv_factorization, pi_Ico_mem_nhds, counit_eq_adjoint, Homeomorph.piCongrLeft_apply_apply, compRightL_apply, inseparable_pi, induced_restrict, ContinuousLinearMap.pi_apply, set_pi_mem_nhds, NumberField.mixedEmbedding.fundamentalCone.isCompact_compactSet, Path.trans_pi_eq_pi_trans, SimplexCategory.continuous_toTopMap, NumberField.mixedEmbedding.negAt_signSet_apply_isComplex, NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure, PiLp.continuous_toLp, ContinuousMap.piMap_apply, GenLoop.loopHomeo_apply, UnitAddTorus.mFourierCoeff_toLp, ContinuousMap.coe_homeoFnOfDiscrete, BoxIntegral.Box.isCompact_Icc, HasOuterApproxClosed.tendsto_apprSeq, Profinite.NobelingProof.fin_comap_jointlySurjective, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, EquicontinuousOn.inducing_uniformOnFun_iff_pi', ContinuousLinearEquiv.piUnique_symm_apply, nhdsKer_singleton_pi, hasStrictFDerivAt_multiset_prod, supConvergenceClass', NumberField.mixedEmbedding.normAtComplexPlaces_polarSpaceCoord_symm, OpenPartialHomeomorph.pi_target, exists_retractionCantorSet, ContinuousLinearMap.isCompact_image_coe_closedBall, ContinuousLinearMap.isClosed_image_coe_closedBall, Profinite.NobelingProof.GoodProducts.spanFin, Profinite.NobelingProof.succ_exact, ContinuousLinearEquiv.finTwoArrow_symm_apply, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, instPathConnectedSpaceElemForallRealStdSimplexOfNonempty, nhdsWithin_pi_univ_eq, ContinuousLinearMap.det_pi, ContinuousLinearMap.iInf_ker_proj, Equicontinuous.tendsto_uniformFun_iff_pi, Profinite.NobelingProof.GoodProducts.smaller_factorization, hasFDerivAt_finCons, Matrix.linfty_opNNNorm_eq_opNNNorm, hasFDerivWithinAt_finCons, MeasureTheory.closedCompactCylinders.isCompact, NumberField.mixedEmbedding.convexBodySum_compact, IsModuleTopology.continuous_bilinear_of_pi_fintype, has_continuous_inv', ContinuousMap.Homotopic.pi, Profinite.NobelingProof.πs'_apply_apply, ContinuousLinearEquiv.piUnique_apply, AddMonoidHom.isClosed_range_coe, continuous_precomp', isCompact_closure_iff, FunOnFinite.continuous_linearMap, SimplexCategory.toTop_obj, NumberField.mixedEmbedding.fundamentalCone.subset_interior_normLeOne, HomotopyGroup.transAt_indep, ProfiniteGrp.denseRange_toLimit, ContinuousLinearMap.proj_apply, NumberField.mixedEmbedding.negAt_signSet_apply_isReal, summable_matrix_diagonal, isClosed_setOf_map_zero, exists_nat_nat_continuous_surjective_of_completeSpace, SimplexCategory.toTop_map, contMDiffWithinAt_pi_space, ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed, differentiableOn_finCons', GenLoop.instContinuousEval, Profinite.NobelingProof.Products.eval_eq, locallyCompactSpace_of_finite, Matrix.linfty_opNNNorm_toMatrix, FundamentalGroupoidFunctor.piToPiTop_map, continuous_apply_apply, LinearIndependent.eventually, Homeomorph.piSplitAt_symm_apply, differentiableAt_apply, ContinuousMultilinearMap.range_toUniformOnFun, ContinuousLinearMap.pi_eq_zero, ContinuousLinearMap.pi_proj, ContinuousAlternatingMap.piEquiv_symm_apply, nhds_pi, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice, differentiableAt_pi'', isClosedMap_restrict_of_compactSpace, OpenPartialHomeomorph.pi_source, PiLp.hasFDerivAt_toLp, ContinuousMap.homeoFnOfDiscrete_symm_apply, Homeomorph.sumArrowHomeomorphProdArrow_symm_apply, CFC.nnrpow_map_pi, ContinuousMap.inseparable_coe, UnitAddTorus.mFourier_add, instNeBotNhdsWithinIoi, SimplexCategory.toTop₀_map, deriv_pi, Homeomorph.funUnique_apply, hasFDerivAt_apply, NumberField.mixedEmbedding.polarCoordReal_source, Profinite.NobelingProof.Products.evalFacProps, hasFTaylorSeriesUpToOn_pi', contMDiffOn_pi_space, PointwiseConvergenceCLM.isEmbedding_coeFn, NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, MeasureTheory.Measure.pi.isLocallyFiniteMeasure, UnitAddTorus.mFourier_zero, instBoundedLENhdsClass, topologicalGroup, Matrix.exp_diagonal, Matrix.l2_opNNNorm_mulVec, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, isCompact_pi_infinite, RestrictedProduct.continuous_rng_of_top, isOpen_pi_iff', instNeBotNhdsWithinIio, Asymptotics.IsLittleOTVS.pi, LinearMap.isClosed_range_coe, TopologicalSpace.productOfMemOpens_isEmbedding, hasFDerivWithinAt_finCons', InfiniteGalois.mulEquivToLimit_symm_continuous, opensMeasurableSpace, PointwiseConvergenceCLM.isInducing_inducingFn, HasSum.matrix_blockDiag', IsHomeomorph.pi_map, ContinuousMultilinearMap.hasBasis_nhds_zero, tendsto_indicator_const_iff_forall_eventually, UnitAddTorus.coeFn_mFourierLp, GenLoop.ext_iff, NumberField.mixedEmbedding.polarCoord_symm_apply, hasDerivAt_update, Homeomorph.piEquivPiSubtypeProd_apply, Finset.continuous_restrict₂, continuous_pi, Continuous.piMap, ContinuousAt.coeFun, MeasureTheory.Measure.pi.isHaarMeasure, AddHom.isClosed_range_coe, InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup, OpenPartialHomeomorph.pi_apply, Preorder.continuous_frestrictLe, isClosed_stdSimplex, UnitAddTorus.mFourier_neg, Function.Surjective.isEmbedding_comp, SimplexCategory.toTop₀_obj, Topology.IsOpenEmbedding.piMap, MeasureTheory.withDensity_tsum, isConnected_univ_pi, Profinite.IndexFunctor.surjective_π_app, MeasureTheory.Measure.instIsLocallyFiniteMeasureForallVolumeOfSigmaFinite, Function.locallyCompactSpace_of_finite, Profinite.NobelingProof.continuous_swapTrue, hasFDerivAt_list_prod', EquicontinuousOn.isClosed_range_pi_of_uniformOnFun', hasStrictFDerivAt_finCons, TopCat.piFan_pt, Path.Homotopic.pi_lift, isClosed_antitoneOn, Module.Basis.equivFunL_symm_apply_repr, Profinite.NobelingProof.iso_map_bijective, closure_upperClosure_comm_pi, isClosed_set_pi, stdSimplex.continuous_map, Homeomorph.toEquiv_piCongrRight, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, ContinuousAlternatingMap.hasStrictFDerivAt, NumberField.mixedEmbedding.negAt_apply_isReal_and_notMem, UniqueDiffOn.pi, ContinuousLinearMapWOT.isInducing_inducingFn, differentiableOn_pi'', DenseRange.piMap, RestrictedProduct.isEmbedding_coe_of_principal, FundamentalGroupoidFunctor.instIsIsoFanGrpdObjTopCatFundamentalGroupoidFunctorPiTopToPiCone, TopCat.piIsoPi_inv_π_apply, GenLoop.continuous_fromLoop, Topology.IsClosedEmbedding.piMap, TopologicalSpace.productOfMemOpens_injective, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_eq, NumberField.mixedEmbedding.volume_preserving_negAt, hasFDerivAt_finCons', instPolynormableSpaceForall, instProperConstSMulForall, NumberField.mixedEmbedding.fundamentalCone.prod_expMapBasis_pow, NumberField.mixedEmbedding.negAt_apply_isComplex, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_closure_subset_compactSet, NumberField.mixedEmbedding.fundamentalCone.continuous_expMap, ContinuousMultilinearMap.coe_continuous, hasStrictDerivAt_finCons', ContinuousLinearEquiv.finTwoArrow_apply, hasStrictDerivAt_finCons, isClosed_setOf_map_smul, Profinite.NobelingProof.Products.eval_πs_image', isClosedEmbedding_update, UnitAddTorus.mFourier_norm, GenLoop.toLoop_apply, ContinuousMultilinearMap.piLinearEquiv_apply, NumberField.mixedEmbedding.normAtComplexPlaces_normAtAllPlaces, pi_Ioc_mem_nhds, isCompact_univ_pi, NumberField.mixedEmbedding.fundamentalCone.expMap_smul, CommRingCat.HomTopology.isClosedEmbedding_hom, isOpen_setOf_affineIndependent, instContinuousStarForall, Set.OrdConnected.null_frontier, TopologicalSpace.productOfMemOpens_isInducing, Profinite.NobelingProof.factors_prod_eq_basis_of_ne, summable_matrix_blockDiagonal', Profinite.NobelingProof.continuous_projRestrict, NumberField.mixedEmbedding.mem_negAt_plusPart_of_mem, ContinuousLinearMap.continuousMultilinearMapOption_apply_eq_self, CFC.rpow_eq_rpow_pi, MeasureTheory.Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite, Module.Basis.equivFunL_apply, PiNat.isOpen_cylinder, EquicontinuousOn.isClosed_range_uniformOnFun_iff_pi, hasFDerivAt_list_prod_finRange', HomotopyGroup.mul_spec, ContinuousMultilinearMap.hasStrictFDerivAt, ContinuousLinearMap.coe_pi, NumberField.mixedEmbedding.fundamentalCone.closure_normLeOne_subset, ContinuousMultilinearMap.pi_apply, ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun, pi_Ici_mem_nhds', Profinite.NobelingProof.continuous_CC'₁, ContinuousLinearMapWOT.isEmbedding_inducingFn, HasSum.matrix_diag, Finset.continuous_restrict, tendsto_indicator_const_iff_forall_eventually', GenLoop.fromLoop_symm_toLoop, NumberField.mixedEmbedding.convexBodySumFun_continuous, CommRingCat.HomTopology.mvPolynomialHomeomorph_symm_apply_hom, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_increments, PiNat.isOpen_iff_dist, exists_nat_bool_continuous_surjective_of_compact, Summable.matrix_blockDiag', MeasureTheory.mem_closedCompactCylinders, tendsto_pi_nhds, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, ProbabilityTheory.Kernel.withDensity_tsum, Homeomorph.piCongrLeft_apply, pi_Ioi_mem_nhds', Summable.matrix_diag, ContinuousMultilinearMap.opNorm_pi, instPreconnectedSpaceForall, differentiableAt_finCons, Profinite.NobelingProof.GoodProducts.span, ContinuousMap.homeoFnOfDiscrete_apply, ContinuousLinearMap.continuousWithinAt_uncurry_of_multilinear, NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm, continuousOn_apply, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, RestrictedProduct.nhds_eq_map_structureMap, CommRingCat.HomTopology.isEmbedding_hom, NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMap, Profinite.NobelingProof.isClosed_C0, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller, pi_eq_generateFrom, instT0Space, MeasureTheory.IsClosed.cylinder, Metric.PiNatEmbed.exists_closed_embedding_to_hilbert_cube, mem_closure_pi, ContinuousMultilinearMap.instContinuousEval, Topology.continuous_reorderRestrictProd, RestrictedProduct.topologicalSpace_eq_of_principal, differentiable_pi, compactSpace, ContinuousAlternatingMap.pi_apply, MulHom.isClosed_range_coe, discreteTopology, deriv_update, Continuous.coeFun, BoundedContinuousFunction.continuous_coe, OpenPartialHomeomorph.pi_toPartialEquiv, thickenedIndicator_tendsto_indicator_closure, NumberField.mixedEmbedding.fundamentalCone.continuous_expMapBasis, isOpen_deltaGenerated_iff, fderivWithin_continuousMultilinearMapCompContinuousLinearMap, hasFDerivAt_single, Topology.IsEmbedding.piMap, Fin.appendHomeomorph_toEquiv, instT35SpaceForall, Submodule.closure_coe_iSup_map_single, instContinuousSMulForall, ContinuousAlternatingMap.hasBasis_nhds_zero, NumberField.mixedEmbedding.fundamentalCone.expMap_symm_apply, NumberField.mixedEmbedding.polarCoord_source, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum, compact_Icc_space', Topology.image_snd_preimageImageRestrict, NumberField.mixedEmbedding.continuous_norm, IsOpenMap.piMap, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, MultilinearMap.continuous_of_bound, borelSpace, NumberField.mixedEmbedding.polarSpaceCoord_symm_apply, stdSimplexHomeomorphUnitInterval_apply_coe, NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces, fderiv_update, dense_pi, DeltaGeneratedSpace.isOpen_iff, WeakDual.coeFn_continuous, isPathConnected_stdSimplex, Homeomorph.piCongrRight_apply, instOrderClosedTopologyForall, isOpen_set_pi, Perfect.exists_nat_bool_injection, continuous_pi_iff, Profinite.NobelingProof.e_mem_of_eq_true, ContinuousLinearMap.continuous_uncurry_of_multilinear, instT3SpaceForall, continuousAdd', Profinite.IndexFunctor.map_comp_π_app, TopologicalSpace.isSeparable_pi, NumberField.mixedEmbedding.mixedSpaceToRealMixedSpace_apply, ContDiffMapSupportedIn.isUniformEmbedding_pi_structureMapCLM, ContinuousMultilinearMap.piEquiv_apply, Asymptotics.isBigOTVS_pi, summable, Profinite.NobelingProof.πs_apply_apply, ContinuousMultilinearMap.isEmbedding_toUniformOnFun, TopologicalSpace.metrizableSpace_pi, GenLoop.toLoop_apply_coe, induced_precomp, NumberField.Units.instDiscrete_unitLattice, NumberField.mixedEmbedding.fundamentalCone.closure_paramSet, Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval, differentiableWithinAt_pi, Homeomorph.piCongrRight_symm, continuousNeg, MeasureTheory.memLp_pi_iff, NumberField.mixedEmbedding.polarCoord_target, ContinuousLinearMap.norm_single, Profinite.NobelingProof.GoodProducts.linearIndependent, NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMapBasis, NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isReal, MeasureTheory.Measure.instIsHaarMeasureForallVolumeOfMeasurableMulOfSigmaFinite, continuous_matrix_diag, continuous_postcomp, Profinite.NobelingProof.GoodProducts.square_commutes, derivWithin_pi, NumberField.mixedEmbedding.negAt_symm, Homeomorph.piUnique_apply, NumberField.InfinitePlace.denseRange_algebraMap_pi, GenLoop.loopHomeo_symm_apply, Set.Equicontinuous.closure, Module.Basis.continuous_toMatrix, isClosed_monotone, NumberField.mixedEmbedding.polarCoord_symm_eq, nhdsWithin_pi_neBot, ContinuousAlternatingMap.piLIE_symm_apply_apply, BoxIntegral.Box.exists_seq_mono_tendsto, instWeaklyLocallyCompactSpaceForallOfFinite, hasStrictFDerivAt_finCons', Profinite.NobelingProof.spanFinBasis.span, continuous_update, instCompletelyRegularSpaceForall, nhdsKer_pi, NumberField.mixedEmbedding.negAt_apply_isReal_and_mem, MeasureTheory.addHaarMeasure_eq_volume_pi, ContinuousMultilinearMap.cont, NumberField.mixedEmbedding.polarSpaceCoord_target', PiLp.toEquiv_homeomorph, hasStrictFDerivAt_list_prod_attach', NumberField.mixedEmbedding.volume_negAt_plusPart, deriv_single, continuous_restrict, Module.Basis.parallelepiped_eq_map, ContinuousAlternatingMap.piLinearEquiv_symm_apply, instR1SpaceForall, hasFDerivAt_update, TopCat.piIsoPi_hom_apply, pi_Iio_mem_nhds', isClosed_setOf_map_inv, ContinuousMap.piEquiv_apply, continuousAt_pi, ProbabilityTheory.iIndepFun.hasGaussianLaw, UniqueDiffOn.univ_pi, instRegularSpaceForall, hasDerivAtFilter_finCons', ContinuousAlternatingMap.range_toAlternatingMap, pi_generateFrom_eq, hasDerivWithinAt_finCons', NumberField.mixedEmbedding.iUnion_negAt_plusPart_union, ContinuousMultilinearMap.norm_iteratedFDeriv_le', hasStrictFDerivAt_finset_prod, WeakBilin.coeFn_continuous, UniqueDiffWithinAt.pi, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal, SmoothBumpCovering.embeddingPiTangent_injOn, pi_le_borel_pi, Continuous.matrix_blockDiag', Matrix.exp_blockDiagonal, hasFDerivAtFilter_finCons, ContinuousLinearMap.pi_comp, UnitAddTorus.mFourierSubalgebra_separatesPoints, ContinuousMap.isHomeomorph_coe, isClosed_setOf_map_mul, continuousMul', NumberField.mixedEmbedding.continuous_normAtPlace, Homeomorph.piFinTwo_apply, PiLp.continuous_ofLp, isCompact_iff, tendstoIccClassNhdsPi, HasSum.matrix_blockDiag, Homeomorph.piCurry_symm_apply, ContinuousMultilinearMap.iteratedFDerivComponent_apply, Profinite.NobelingProof.isClosed_proj, induced_restrict_sUnion, ContinuousMultilinearMap.hasFDerivAt, HomotopyGroup.one_def, PolishSpace.exists_nat_nat_continuous_surjective, MonoidHom.isClosed_range_coe, pi_Iic_mem_nhds, ContinuousLinearMap.continuousOn_uncurry_of_multilinear, NumberField.mixedEmbedding.injective_mixedSpaceOfRealSpace, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_pos, TopologicalSpace.instSecondCountableTopologyForallOfCountable, ContinuousLinearMap.proj_pi, ContinuousMultilinearMap.piₗᵢ_symm_apply, nhdsWithin_pi_eq, NumberField.mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace, CFC.nnrpow_eq_nnrpow_pi, Profinite.NobelingProof.isClosed_C', ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis, SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, IsClosed.exists_nat_bool_injection_of_not_countable, fderiv_continuousMultilinearMapCompContinuousLinearMap, RestrictedProduct.continuous_dom_pi, ContinuousAlternatingMap.hasBasis_nhds_zero_of_basis, NumberField.mixedEmbedding.fundamentalCone.expMap_apply, LinearMap.continuous_on_pi, Matrix.linfty_opNorm_toMatrix, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, ContinuousMultilinearMap.opNNNorm_pi, stdSimplexHomeomorphUnitInterval_one, ContinuousMultilinearMap.coe_pi, ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap, Profinite.NobelingProof.continuous_projRestricts, ProbabilityTheory.iIndepFun_iff_charFunDual_pi', instBoundedGENhdsClass, TopologicalSpace.IsCompletelyPseudoMetrizableSpace.pi_countable, continuousMul, Profinite.NobelingProof.GoodProducts.smaller_mono, FunOnFinite.continuous_map, HomotopyGroup.inv_spec, closure_pi_set, hasSum, instCompactIccSpaceForall, OpenPartialHomeomorph.pi_symm_apply, mapsTo_tangentConeAt_pi, continuous_single, topologicalAddGroup, ContinuousLinearMap.hasFDerivAt_uncurry_of_multilinear, induced_to_pi, tendsto_indicator_const_iff_tendsto_pi_pure, SmoothBumpCovering.embeddingPiTangent_injective, Continuous.matrix_diag, HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap, Profinite.NobelingProof.GoodProducts.linearIndependentEmpty, PiLp.hasFDerivAt_ofLp, NumberField.mixedEmbedding.fundamentalCone.injective_expMapBasis, UniqueDiffWithinAt.univ_pi, FundamentalGroupoidFunctor.piToPiTop_obj_as, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex, differentiableAt_finCons', locallyCompactSpace, NumberField.mixedEmbedding.lintegral_comp_polarCoordReal_symm, TopCat.partialSections.closed, NumberField.mixedEmbedding.measurable_polarCoord_symm, cfc_map_pi, NumberField.mixedEmbedding.fundamentalCone.expMap_source, withSeminorms_pi, Homeomorph.piUnique_symm_apply, Homeomorph.piEquivPiSubtypeProd_symm_apply, ProfiniteGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemSubgroupLimitConePtAux, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply'', ContinuousLinearMap.coe_proj, tendsto_mulIndicator_thickening_mulIndicator_closure, FundamentalGroupoidFunctor.piIso_inv, MeasureTheory.MemLp.of_eval, exists_compact_superset_iff, hasDerivAtFilter_finCons, det_fderivPiPolarCoordSymm, cantorToHilbert_continuous, ContinuousAddMonoidHom.isClosedEmbedding_coe, infConvergenceClass, ContinuousLinearMap.isCompact_closure_image_coe_of_bounded, NumberField.mixedEmbedding.polarCoord_apply, NumberField.mixedEmbedding.hasFDerivAt_polarCoordReal_symm, nhdsWithin_pi_eq_bot, ContinuousLinearMapWOT.continuous_inducingFn, tendsto_indicator_cthickening_indicator_closure, NumberField.mixedEmbedding.continuous_normAtAllPlaces, MeasureTheory.charFunDual_eq_pi_iff', hasFDerivAt_pi_polarCoord_symm, Profinite.NobelingProof.GoodProducts.span_iff_products, IsUpperSet.null_frontier, MeasureTheory.closedCompactCylinders.isClosed, hasStrictDerivAt_pi, Matrix.linfty_opNorm_eq_opNorm, Profinite.NobelingProof.GoodProducts.sum_equiv_comp_eval_eq_elim, MeasureTheory.isAddHaarMeasure_volume_pi, continuousWithinAt_pi, NumberField.mixedEmbedding.normAtPlace_negAt, ContinuousLinearMap.norm_pi_le_of_le, continuous_apply, inducing_iInf_to_pi, isClosed_setOf_map_neg, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply, instContinuousConstVAddForall, hasFDerivWithinAt_pi, GenLoop.Homotopic.equiv, differentiableWithinAt_apply, ContinuousAlternatingMap.hasFDerivWithinAt, ContinuousMultilinearMap.piEquiv_symm_apply, NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ, RestrictedProduct.isEmbedding_coe_of_top, continuousAt_apply, TopCat.piIsoPi_inv_π, ContinuousLinearMap.norm_single_le_one, NumberField.mixedEmbedding.polarSpaceCoord_apply, NumberField.mixedEmbedding.negAt_apply_norm_isReal, Topology.IsInducing.piMap, CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_fst, hasStrictFDerivAt_list_prod, ContinuousMultilinearMap.toUniformOnFun_toFun, hasDerivAtFilter_pi, instSigmaCompactSpaceForallOfFinite, NumberField.mixedEmbedding.fundamentalCone.expMap_add, instAlexandrovDiscreteOfFinite, hasDerivAt_finCons', NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply, instT1SpaceForall, Profinite.NobelingProof.CC_comp_zero, differentiable_pi'', UnitAddTorus.span_mFourier_closure_eq_top, ContinuousMap.homeoFnOfDiscrete_symm_apply_apply, hasDerivAt_single, RestrictedProduct.topologicalSpace_eq_of_bot, PiLp.coe_symm_continuousLinearEquiv, differentiableOn_apply, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_snd, Profinite.NobelingProof.eval_eq_πJ, differentiableAt_pi, Fin.appendHomeomorph_symm_apply, Profinite.NobelingProof.continuous_CC'₀, ContinuousWithinAt.coeFun, continuousOn_pi', Profinite.NobelingProof.Products.evalFacProp, MeasureTheory.AnalyticSet_def, ZSpan.discreteTopology_pi_basisFun, continuous_restrict₂, MeasureTheory.Measure.pi.isAddHaarMeasure, ContinuousLinearMap.pi_proj_comp, MeasureTheory.integrable_pi_iff, NumberField.mixedEmbedding.polarSpaceCoord_source, Homeomorph.piCongrLeft_refl, Profinite.NobelingProof.Products.evalCons, Real.continuous_ofDigits, ContinuousMap.pi_eval, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image, TopologicalSpace.instSeparableSpaceForallOfCountable, hasFDerivAtFilter_finCons', CFC.rpow_map_pi, UnitAddTorus.mFourier_single, Cube.insertAt_boundary, instIsTopologicalRing, pi_Ici_mem_nhds, Profinite.NobelingProof.one_sub_e_mem_of_false, isClosed_antitone, ProfiniteGrp.toLimitFun_continuous, contMDiff_pi_space, NumberField.mixedEmbedding.polarCoord_target_eq_polarCoordReal_target, induced_precomp', set_pi_mem_nhds_iff, continuous_mulSingle, MeasureTheory.charFunDual_pi, NumberField.mixedEmbedding.fundamentalCone.compactSet_ae, NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, NumberField.mixedEmbedding.instIsAddHaarMeasureRealMixedSpaceVolume, TopologicalSpace.instFirstCountableTopologyForallOfCountable, InfiniteGalois.algEquivToLimit_continuous, ContinuousAlternatingMap.differentiable, ENNReal.tsum_apply, RestrictedProduct.isEmbedding_coe_of_bot, CFC.sqrt_map_pi, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_expMap_symm, isCompact_iff_of_isClosed, Profinite.NobelingProof.injective_πs, ContinuousAlternatingMap.continuousMapClass, NumberField.mixedEmbedding.measurableSet_negAt_plusPart, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_symm_apply, pi_Ioc_mem_nhds', ContinuousAt.piMap, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, Profinite.Nobeling.isClosedEmbedding, interior_pi_set, ContinuousMultilinearMap.piₗᵢ_apply, Module.Basis.opNNNorm_le, infConvergenceClass', Profinite.NobelingProof.coe_πs', Profinite.NobelingProof.continuous_proj, Homeomorph.funSplitAt_apply, ContinuousMap.Homotopic.piMap, hasStrictFDerivAt_list_prod', Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun_bijective, EquicontinuousOn.isInducing_uniformOnFun_iff_pi, NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_apply, Set.UniformEquicontinuous.closure, continuous_coeFun, Fin.continuous_append, pi_Icc_mem_nhds, RestrictedProduct.nhds_zero_eq_map_structureMap, isTopologicalBasis_pi, MeasureTheory.Measure.instIsOpenPosMeasureForallVolumeOfSigmaFinite, Matrix.exp_blockDiagonal', NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_image_preimage_expMapBasis, Matrix.diagonal_tsum, ContinuousMap.eval_apply, pi_Ioi_mem_nhds, ContinuousMultilinearMap.continuousMapClass, PiLp.hasStrictFDerivAt_ofLp, ContinuousMultilinearMap.fderivCompContinuousLinearMap_apply, Module.Basis.continuous_coe_repr, NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace, NumberField.mixedEmbedding.det_fderivPolarCoordRealSymm, nhdsWithin_pi_eq', Module.Basis.opNorm_le, RestrictedProduct.topologicalSpace_eq_of_top, differentiable_finCons, ContinuousAlternatingMap.opNorm_pi, NumberField.mixedEmbedding.fundamentalCone.expMap_sum, Profinite.NobelingProof.list_prod_apply, instContinuousVAddForall, IsOpenQuotientMap.piMap, IsModuleTopology.instPi, PiNat.exists_retraction_of_isClosed, instR0SpaceForall, PiLp.continuousLinearEquiv_apply, ContinuousAlternatingMap.instContinuousEval, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne_eq_image, ContinuousLinearMap.coe_pi', tendsto_indicator_const_iff_tendsto_pi_pure', Submodule.topologicalClosure_iSup_map_single, instContinuousConstSMulForall, instContinuousAddForallOfIsTopologicalSemiring, ContinuousAlternatingMap.hasFDerivAt, IsClosed.upperClosure_pi, ContinuousLinearMap.pi_zero, opensMeasurableSpace_of_subsingleton, differentiableOn_finCons, Matrix.blockDiagonal'_tsum, Homeomorph.funUnique_symm_apply, pi_Ioo_mem_nhds', hasDerivAt_pi, ContinuousMap.HomotopyRel.pi_apply, pi_Icc_mem_nhds', IsLowerSet.null_frontier, NumberField.mixedEmbedding.polarCoordReal_target, hasDerivWithinAt_finCons, contMDiffAt_pi_space, TopologicalSpace.pseudoMetrizableSpace_pi, fderiv_pi, Set.EquicontinuousOn.closure, Homeomorph.piSplitAt_apply, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_range, ContinuousLinearMap.isCompact_image_coe_of_bounded_of_weak_closed, Profinite.NobelingProof.GoodProducts.max_eq_eval, isClosed_monotoneOn, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_source, continuousAdd, tendsto_mulIndicator_cthickening_mulIndicator_closure, continuous_postcomp', WeakDual.isClosed_image_coe_of_bounded_of_closed, NumberField.mixedEmbedding.integral_comp_polarCoord_symm, SmoothBumpCovering.embeddingPiTangent_coe, ContinuousAlternatingMap.coe_continuous, piChartedSpace_chartAt, NumberField.mixedEmbedding.fundamentalCone.expMap_pos, supConvergenceClass, Topology.CWComplex.continuousOn_symm, FundamentalGroupoidFunctor.proj_map, Homeomorph.piFinTwo_symm_apply, hasFDerivAtFilter_pi', isClosed_setOf_lipschitzWith, NumberField.mixedEmbedding.norm_negAt, ContinuousMultilinearMap.isUniformInducing_toUniformOnFun, ContinuousAlternatingMap.piLinearEquiv_apply, GenLoop.boundary, GenLoop.homotopyFrom_apply, GenLoop.const_apply, Profinite.NobelingProof.GoodProducts.linearIndependentSingleton, stdSimplex.instCompactSpace_coe, TopologicalSpace.IsCompletelyMetrizableSpace.pi_countable, NumberField.mixedEmbedding.fundamentalCone.normLeOne_eq_preimage, TopCat.piFan_π_app, GenLoop.fromLoop_coe, hasFDerivAt_pi', borelSpace_of_subsingleton, ContinuousMultilinearMap.hasStrictFDerivAt_uncurry, Preorder.continuous_restrictLe, tendsto_indicator_thickening_indicator_closure, continuousOn_pi, Profinite.NobelingProof.Products.eval_πs_image, MeasureTheory.Measure.instIsFiniteMeasureOnCompactsForallVolumeOfSigmaFinite, MeasureTheory.Measure.pi.isOpenPosMeasure, RestrictedProduct.continuous_rng_of_bot, Measurable.ennreal_tsum', instNeBotNhdsWithinUnivPi, closure_lowerClosure_comm_pi, Profinite.NobelingProof.isClosed_C1, ProfiniteAddGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemAddSubgroupLimitConePtAux, NumberField.mixedEmbedding.integral_comp_polarCoordReal_symm, Fin.consEquivL_symm_apply, NumberField.mixedEmbedding.fundamentalCone.compactSet_eq_union, fderiv_single, GenLoop.homotopicTo, HasOuterApproxClosed.exAppr, Preorder.continuous_frestrictLe₂, hasFDerivAt_list_prod_attach', Set.EquicontinuousAt.closure, ContinuousLinearEquiv.piCongrRight_symm_apply, NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace, GenLoop.continuous_toLoop, NumberField.mixedEmbedding.measurable_polarSpaceCoord_symm, isOpen_setOf_linearIndependent, AnalyticOnNhd.eval_continuousLinearMap, hasStrictFDerivAt_pi, GenLoop.fromLoop_trans_toLoop, Asymptotics.isLittleOTVS_pi, Real.fromBinary_continuous, totallyDisconnectedSpace, FundamentalGroupoidFunctor.coneDiscreteComp_obj_mapCone, CantorScheme.VanishingDiam.map_continuous, NumberField.mixedEmbedding.fundamentalCone.injective_expMap, ContinuousLinearEquiv.coe_funUnique_symm, TopologicalSpace.IsSeparable.univ_pi, ContinuousLinearEquiv.piCongrRight_apply, Profinite.NobelingProof.factors_prod_eq_basis, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne, isClosed_setOf_map_one, hasDerivAt_finCons, NumberField.mixedEmbedding.disjoint_negAt_plusPart, ContinuousLinearEquiv.piFinTwo_symm_apply, Preorder.continuous_restrictLe₂, Profinite.NobelingProof.factors_prod_eq_basis_of_eq, Asymptotics.IsBigOTVS.pi, summable_matrix_blockDiagonal, Profinite.NobelingProof.GoodProducts.union, specializes_pi, exp_def, ContinuousLinearEquiv.coe_funUnique, MvPolynomial.continuous_eval, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_nonneg, hasFDerivAt_pi, ContinuousMonoidHom.isClosedEmbedding_coe, CategoryTheory.PreGaloisCategory.autEmbedding_isClosedEmbedding, GenLoop.instContinuousEvalConst, Set.EquicontinuousWithinAt.closure, differentiableWithinAt_finCons, DeltaGeneratedSpace.continuous_iff, NumberField.mixedEmbedding.fundamentalCone.logMap_normAtAllPlaces, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, ContinuousLinearMap.continuousAt_uncurry_of_multilinear, RestrictedProduct.isEmbedding_structureMap, hasFDerivWithinAt_apply, NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlaces, TopCat.piIsoPi_inv_π_assoc, pi_generateFrom_eq_finite, multipliable, ContinuousLinearEquiv.piFinTwo_apply, MeasureTheory.Measure.pi.isFiniteMeasureOnCompacts, Metric.PiNatEmbed.exists_embedding_to_hilbert_cube, Profinite.NobelingProof.GoodProducts.max_eq_eval_unapply, isPreconnected_univ_pi, instIsTopologicalAddTorsorForall, Profinite.NobelingProof.succ_mono, NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply, NumberField.mixedEmbedding.fundamentalCone.closure_paramSet_ae_interior, CategoryTheory.PreGaloisCategory.autEmbedding_range_isClosed, coe_exp, NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm, PiLp.hasStrictFDerivAt_toLp, hasFDerivAt_finset_prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_postcomp 📖	mathematical	Continuous	topologicalSpace	—	continuous_postcomp'
continuous_postcomp' 📖	mathematical	Continuous	topologicalSpace	—	continuous_pi Continuous.comp continuous_apply
continuous_precomp 📖	mathematical	—	Continuous topologicalSpace	—	continuous_precomp'
continuous_precomp' 📖	mathematical	—	Continuous topologicalSpace	—	continuous_pi continuous_apply
continuous_restrict 📖	mathematical	—	Continuous topologicalSpace Set.Elem Set Set.instMembership Set.restrict	—	continuous_precomp'
continuous_restrict_apply 📖	mathematical	Continuous	Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.restrict	—	Continuous.comp continuous_subtype_val
continuous_restrict₂ 📖	mathematical	Set Set.instHasSubset	Continuous topologicalSpace Set.Elem Set.instMembership Set.restrict₂	—	continuous_pi continuous_apply
continuous_restrict₂_apply 📖	mathematical	Set Set.instHasSubset Continuous Set.Elem instTopologicalSpaceSubtype Set.instMembership	Set.restrict₂	—	Continuous.comp continuous_inclusion
discreteTopology 📖	mathematical	DiscreteTopology	topologicalSpace	—	discreteTopology_iff_isOpen_singleton Set.univ_pi_singleton isOpen_set_pi Set.finite_univ isOpen_discrete
induced_precomp 📖	mathematical	—	TopologicalSpace.induced topologicalSpace iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice Function.eval	—	induced_precomp'
induced_precomp' 📖	mathematical	—	TopologicalSpace.induced topologicalSpace iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice Function.eval	—	induced_iInf induced_compose
induced_restrict 📖	mathematical	—	TopologicalSpace.induced Set.restrict topologicalSpace Set.Elem Set Set.instMembership iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice Function.eval	—	iInf_congr_Prop induced_precomp'
induced_restrict_sUnion 📖	mathematical	—	TopologicalSpace.induced Set.restrict Set.sUnion topologicalSpace Set.Elem Set Set.instMembership iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	induced_restrict iInf_congr_Prop iInf_sUnion

Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preimage_mem_nhds 📖	mathematical	Set Filter Filter.instMembership nhds instTopologicalSpaceQuotient	Set.preimage	—	preimage_nhds_coinduced

SetLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDiscrete_iff_discreteTopology 📖	mathematical	—	IsDiscrete coe DiscreteTopology instMembership instTopologicalSpaceSubtype	—	IsDiscrete.to_subtype

Sigma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discreteTopology 📖	mathematical	DiscreteTopology	instTopologicalSpaceSigma	—	iSup_eq_bot DiscreteTopology.eq_bot coinduced_bot
nhds_eq 📖	mathematical	—	nhds instTopologicalSpaceSigma Filter.map	—	—
nhds_mk 📖	mathematical	—	nhds instTopologicalSpaceSigma Filter.map	—	Topology.IsOpenEmbedding.map_nhds_eq Topology.IsOpenEmbedding.sigmaMk

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dense_iff 📖	mathematical	—	Dense Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.instHasSubset closure Set.image	—	Topology.IsInducing.dense_iff Topology.IsInducing.subtypeVal SetCoe.forall

Sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discreteTopology 📖	mathematical	—	DiscreteTopology instTopologicalSpaceSum	—	sup_eq_bot_iff DiscreteTopology.eq_bot coinduced_bot

Topology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isEmbedding_sigmaMap 📖	mathematical	—	IsEmbedding instTopologicalSpaceSigma Sigma.map	—	isInducing_sigmaMap Function.Injective.sigma_map_iff
isInducing_sigmaMap 📖	mathematical	—	IsInducing instTopologicalSpaceSigma Sigma.map	—	Filter.map_sigma_mk_comap sigma_mk_injective
isOpenEmbedding_sigmaMap 📖	mathematical	—	IsOpenEmbedding instTopologicalSpaceSigma Sigma.map	—	isEmbedding_sigmaMap

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inclusion 📖	mathematical	Set Set.instHasSubset	Topology.IsClosedEmbedding Set.Elem instTopologicalSpaceSubtype Set.instMembership Set.inclusion	—	Topology.IsEmbedding.inclusion Set.range_inclusion
piMap 📖	mathematical	Topology.IsClosedEmbedding	Pi.topologicalSpace Pi.map	—	Topology.IsEmbedding.piMap toIsEmbedding Set.range_piMap isClosed_set_pi isClosed_range
sigmaMk 📖	mathematical	—	Topology.IsClosedEmbedding instTopologicalSpaceSigma	—	of_continuous_injective_isClosedMap continuous_sigmaMk sigma_mk_injective isClosedMap_sigmaMk
subtypeVal 📖	mathematical	—	Topology.IsClosedEmbedding instTopologicalSpaceSubtype	—	Topology.IsEmbedding.subtypeVal Subtype.range_coe_subtype
uliftDown 📖	mathematical	—	Topology.IsClosedEmbedding ULift.topologicalSpace	—	Topology.IsEmbedding.uliftDown Function.Surjective.range_eq ULift.down_surjective

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codRestrict 📖	mathematical	Topology.IsEmbedding Set Set.instMembership	Set.Elem instTopologicalSpaceSubtype Set.codRestrict	—	of_comp Continuous.codRestrict continuous continuous_subtype_val
inclusion 📖	mathematical	Set Set.instHasSubset	Topology.IsEmbedding Set.Elem instTopologicalSpaceSubtype Set.instMembership Set.inclusion	—	codRestrict subtypeVal
piMap 📖	mathematical	Topology.IsEmbedding	Pi.topologicalSpace Pi.map	—	Topology.IsInducing.piMap toIsInducing Function.Injective.piMap injective
restrict 📖	mathematical	Topology.IsEmbedding Set.MapsTo	Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.MapsTo.restrict	—	of_comp Continuous.restrict continuous continuous_subtype_val comp subtypeVal
sigmaMk 📖	mathematical	—	Topology.IsEmbedding instTopologicalSpaceSigma	—	Topology.IsClosedEmbedding.toIsEmbedding Topology.IsClosedEmbedding.sigmaMk
subtypeVal 📖	mathematical	—	Topology.IsEmbedding instTopologicalSpaceSubtype	—	Topology.IsInducing.subtypeVal Subtype.coe_injective
uliftDown 📖	mathematical	—	Topology.IsEmbedding ULift.topologicalSpace	—	ULift.down_injective

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codRestrict 📖	mathematical	Topology.IsInducing Set Set.instMembership	Set.Elem instTopologicalSpaceSubtype Set.codRestrict	—	of_comp Continuous.codRestrict continuous continuous_subtype_val
of_codRestrict 📖	—	Set Set.instMembership Topology.IsInducing Set.Elem instTopologicalSpaceSubtype Set.codRestrict	—	—	comp subtypeVal
piMap 📖	mathematical	Topology.IsInducing	Pi.topologicalSpace Pi.map	—	nhds_pi nhds_eq_comap Filter.pi_comap
subtypeVal 📖	mathematical	—	Topology.IsInducing Set Set.instMembership instTopologicalSpaceSubtype	—	—

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inclusion 📖	mathematical	Set Set.instHasSubset IsOpen Set.Elem instTopologicalSpaceSubtype Set.instMembership Set.preimage	Topology.IsOpenEmbedding Set.inclusion	—	Topology.IsEmbedding.inclusion Set.range_inclusion
piMap 📖	mathematical	Topology.IsOpenEmbedding	Pi.topologicalSpace Pi.map	—	Topology.IsEmbedding.piMap toIsEmbedding Set.range_piMap isOpen_set_pi Set.finite_univ isOpen_range
restrict 📖	mathematical	Topology.IsOpenEmbedding Set.MapsTo IsOpen	Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.MapsTo.restrict	—	Topology.IsEmbedding.restrict isEmbedding Set.MapsTo.range_restrict Continuous.isOpen_preimage continuous_subtype_val isOpenMap
sigmaMk 📖	mathematical	—	Topology.IsOpenEmbedding instTopologicalSpaceSigma	—	of_continuous_injective_isOpenMap continuous_sigmaMk sigma_mk_injective isOpenMap_sigmaMk

Topology.IsQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictPreimage_isOpen 📖	mathematical	Topology.IsQuotientMap IsOpen	Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage	—	Topology.isQuotientMap_iff Function.Surjective.restrictPreimage surjective Topology.IsOpenEmbedding.isOpen_iff_image_isOpen IsOpen.isOpenEmbedding_subtypeVal isOpen_preimage IsOpen.preimage continuous Set.image_val_preimage_restrictPreimage

ULift

Definitions

Name	Category	Theorems
topologicalSpace 📖	CompOp	34 math math: ContinuousMap.Homotopy.apply_zero_path, instDiscreteTopologyULift, ContinuousMap.Homotopy.evalAt_eq, instIsTopologicalRingULift, ContinuousMap.Homotopy.ulift_apply, Topology.IsOpenEmbedding.uliftMap, compactSpace, continuous_uliftUp, Topology.IsClosedEmbedding.uliftMap, ContinuousMap.Homotopy.apply_one_path, instContinuousVAddULift, instIsTopologicalSemiringULift, instContinuousAddULift, Topology.IsEmbedding.uliftMap, instSigmaCompactSpaceULift, instT3Space, Topology.IsEmbedding.uliftDown, instContinuousSMulULift, instCompletelyNormalSpace, instBorelSpace, continuous_uliftDown, instT2Space, instIsTopologicalGroupULift, instContinuousInvULift, instT0Space, instContinuousNegULift, isClosed_iff, continuous_uliftMap, isOpen_iff, instT5Space, Topology.IsClosedEmbedding.uliftDown, instT4Space, instContinuousMulULift, instT1Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed_iff 📖	mathematical	—	IsClosed topologicalSpace Set.preimage	—	isOpen_compl_iff isOpen_iff Set.preimage_compl
isOpen_iff 📖	mathematical	—	IsOpen topologicalSpace Set.preimage	—	topologicalSpace.eq_1 Equiv.ulift_apply Equiv.coinduced_symm isOpen_coinduced

(root)

Definitions

Name	Category	Theorems
CofiniteTopology 📖	CompOp	12 math math: instT1SpaceCofiniteTopology, CofiniteTopology.continuous_of, CofiniteTopology.mem_nhds_iff, CofiniteTopology.nhds_eq, TopologicalSpace.instNoetherianSpaceCofiniteTopology, t1Space_TFAE, CofiniteTopology.isClosed_iff, instIrreducibleSpaceCofiniteTopologyOfInfinite, t1Space_iff_continuous_cofinite_of, OnePoint.not_continuous_cofiniteTopology_of_symm, CofiniteTopology.isOpen_iff, CofiniteTopology.isOpen_iff'
IsDiscrete 📖	CompData	25 math math: IsDiscrete.of_openPartialHomeomorph, isDiscrete_iff_nhdsWithin, IsEmbedding.isDiscrete_range, Algebra.QuasiFinite.isDiscrete_comap_preimage_singleton, mem_codiscrete', AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage_singleton, Function.locallyFinsuppWithin.discreteSupport, DiscreteTopology.isDiscrete, isClosed_and_discrete_iff, IsDiscrete.univ, Set.Finite.isDiscrete_of_subset_closedPoints, isDiscrete_univ_iff, IsDiscrete.of_nhdsWithin, IsOpenMap.isDiscrete_range, Set.Finite.isDiscrete, AlgebraicGeometry.locallyQuasiFinite_iff_isDiscrete_preimage_singleton, isDiscrete_iff_forall_exists_isOpen, isDiscrete_iff_nhdsNE, isDiscrete_iff_discreteTopology, IsLocalHomeomorphOn.isDiscrete_image_iff, IsClosed.tendsto_coe_cofinite_iff, Set.Subsingleton.isDiscrete, SetLike.isDiscrete_iff_discreteTopology, isDiscrete_of_codiscreteWithin, discreteTopology_of_codiscreteWithin
instTopologicalSpaceAdditive 📖	CompOp	17 math math: nhds_ofMul, instCompactSpaceAdditive, isClosedMap_ofMul, instContinuousAddAdditiveOfContinuousMul, instDiscreteTopologyAdditive, instNoncompactSpaceAdditive, instIsTopologicalAddGroupAdditiveOfIsTopologicalGroup, instLocallyCompactSpaceAdditive, continuous_ofMul, isOpenMap_ofMul, instTotallyDisconnectedSpaceAdditive, instWeaklyLocallyCompactSpaceAdditive, isClosedMap_toMul, continuous_toMul, nhds_toMul, instContinuousNegAdditiveOfContinuousInv, isOpenMap_toMul
instTopologicalSpaceMultiplicative 📖	CompOp	17 math math: instWeaklyLocallyCompactSpaceMultiplicative, instIsTopologicalGroupMultiplicativeOfIsTopologicalAddGroup, instContinuousInvMultiplicativeOfContinuousNeg, continuous_toAdd, instTotallyDisconnectedSpaceMultiplicative, instCompactSpaceMultiplicative, isClosedMap_ofAdd, nhds_toAdd, isClosedMap_toAdd, isOpenMap_toAdd, instLocallyCompactSpaceMultiplicative, instNoncompactSpaceMultiplicative, isOpenMap_ofAdd, instDiscreteTopologyMultiplicative, nhds_ofAdd, instContinuousMulMultiplicativeOfContinuousAdd, continuous_ofAdd
instTopologicalSpaceQuot 📖	CompOp	10 math math: TopologicalSpace.instSeparableSpaceQuot, continuous_quot_lift, Quot.locPathConnectedSpace, Quot.isGeneratedBy, continuous_quot_mk, Quot.compactSpace, Quot.LindelofSpace, Quot.deltaGeneratedSpace, Quot.lindelofSpace, isQuotientMap_quot_mk
instTopologicalSpaceQuotient 📖	CompOp	43 math math: Quotient.compactSpace, Quotient.instPathConnectedSpace, isOpenMap_quotient_mk'_add, isQuotientCoveringMap_quotientMk_of_properlyDiscontinuousSMul, Topology.IsQuotientMap.lift_apply, isQuotientMap_quotient_mk', Topology.IsQuotientMap.homeomorph_apply, Topology.IsQuotientMap.homeomorph_symm_apply, Quotient.instSequentialSpace, ContinuousConstSMul.secondCountableTopology, continuous_quotient_mk', AddAction.isClosedMap_quotient, Quotient.locPathConnectedSpace, isAddQuotientCoveringMap_quotientMk_of_properlyDiscontinuousVAdd, Quotient.isGeneratedBy, AddAction.isOpenQuotientMap_quotientMk, DenseRange.quotient, ContinuousConstVAdd.secondCountableTopology, t2Space_quotient_addAction_of_properVAdd, isOpenMap_quotient_mk'_mul, Quotient.instAlexandrovDiscrete, t2Space_of_properlyDiscontinuousVAdd_of_t2Space, Quotient.instConnectedSpace, MulAction.isOpenQuotientMap_quotientMk, Function.RightInverse.homeomorph_symm_apply, Quotient.deltaGeneratedSpace, Continuous.quotient_map', continuous_map_sInf, t2Space_quotient_mulAction_of_properSMul, TopologicalSpace.instSeparableSpaceQuotient, isCoveringMapOn_quotientMk_of_properlyDiscontinuousVAdd, continuous_map_of_le, isCoveringMapOn_quotientMk_of_properlyDiscontinuousSMul, Quotient.lindelofSpace, Continuous.quotient_lift, Quotient.LindelofSpace, instUCompactlyGeneratedSpaceQuotient, Function.RightInverse.homeomorph_apply, MulAction.isClosedMap_quotient, Dense.quotient, Continuous.quotient_liftOn', Quotient.borelSpace, t2Space_of_properlyDiscontinuousSMul_of_t2Space
instTopologicalSpaceSigma 📖	CompOp	77 math math: Sigma.isPreconnected_iff, isClosedMap_sigmaMk, ContinuousMap.exists_lift_sigma, instUCompactlyGeneratedSpaceSigma, TopCat.sigmaIsoSigma_hom_ι, deltaGenerated_eq_coinduced, TopologicalSpace.instSecondCountableTopologySigmaOfCountable, AlgebraicGeometry.sigmaMk_mk, TopologicalSpace.Fiber.sigmaIsoHom_inj, continuous_sigma_map, comap_sigmaMk_nhds, isOpenMap_sigma_map, TopCat.sigmaCofan_ι_app, instCompactSpaceSigmaOfFinite, instLindelofSpaceSigmaOfCountable, Sigma.instAlexandrovDiscrete, TopCat.sigmaIsoSigma_inv_apply, Topology.isInducing_sigmaMap, inducing_sigma, Stonean.effectiveEpiFamily_tfae, continuous_sigmaMk, Topology.IsClosedEmbedding.sigmaMk, Topology.isEmbedding_sigmaMap, IsHomeomorph.sigmaMap, ContinuousMap.isEmbedding_sigmaMk_comp, TopologicalSpace.Opens.isBasis_sigma, TopCat.sigmaIsoSigma_hom_ι_assoc, IsCompactOpenCovered.iff_isCompactOpenCovered_sigmaMk, Topology.IsEmbedding.sigmaMk, Continuous.sigma_map, instCompactlyGeneratedSpaceSigma, ContinuousMap.sigmaEquiv_symm_apply, TopologicalSpace.Fiber.sigmaIsoHom_apply, isClopen_range_sigmaMk, ContinuousMap.sigma_apply, ContinuousMap.sigmaMk_apply, isClosed_range_sigmaMk, ContinuousMap.sigmaEquiv_apply, instSigmaCompactSpaceSigmaOfCountable, continuous_sigma_iff, Sigma.nhds_mk, ContinuousMap.piComparison_fac, instExtremallyDisconnected, Sigma.instSequentialSpace, Set.isCompact_sigma, Homeomorph.sigmaProdDistrib_symm_apply, TopologicalSpace.IsTopologicalBasis.sigma, Sigma.locPathConnectedSpace, isClosed_sigma_iff, ContinuousMap.sigmaCodHomeomorph_symm_apply, isOpenMap_sigmaMk, Sigma.nhds_eq, CompHausLike.isIsoSigmaComparison, Topology.IsOpenEmbedding.sigmaMk, instTotallyDisconnectedSpaceSigma, TopologicalSpace.Fiber.sigmaIsoHom_surj, isOpen_range_sigmaMk, Sigma.t2Space, PrespectralSpace.sigma, continuous_sigma, TopCat.sigmaCofan_pt, Sigma.discreteTopology, isOpenMap_sigma, Topology.isOpenEmbedding_sigmaMap, Homeomorph.toEquiv_sigmaProdDistrib, TopCat.sigmaIsoSigma_hom_ι_apply, isOpen_sigma_iff, Sigma.isConnected_iff, CompHaus.effectiveEpiFamily_tfae, isOpen_sigma_fst_preimage, Sigma.isGeneratedBy, Homeomorph.sigmaProdDistrib_apply, Profinite.effectiveEpiFamily_tfae, Sigma.deltaGeneratedSpace, TopologicalSpace.IsCompletelyMetrizableSpace.sigma, Metric.Sigma.isOpen_iff, CompHausLike.instHasPropSigma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_subtype 📖	mathematical	—	Set Set.instMembership closure instTopologicalSpaceSubtype Set.image	—	closure_induced
comap_nhdsWithin_range 📖	mathematical	—	Filter.comap nhdsWithin Set.range nhds	—	Filter.comap_inf_principal_range
comap_sigmaMk_nhds 📖	mathematical	—	Filter.comap nhds instTopologicalSpaceSigma	—	Topology.IsInducing.nhds_eq_comap Topology.IsEmbedding.toIsInducing Topology.IsEmbedding.sigmaMk
continuousAt_apply 📖	mathematical	—	ContinuousAt Pi.topologicalSpace	—	Continuous.continuousAt continuous_apply
continuousAt_codRestrict_iff 📖	mathematical	Set Set.instMembership	ContinuousAt Set.Elem instTopologicalSpaceSubtype Set.codRestrict	—	Topology.IsInducing.continuousAt_iff Topology.IsInducing.subtypeVal
continuousAt_pi 📖	mathematical	—	ContinuousAt Pi.topologicalSpace	—	tendsto_pi_nhds
continuousAt_pi' 📖	mathematical	ContinuousAt	Pi.topologicalSpace	—	continuousAt_pi
continuousAt_subtype_val 📖	mathematical	—	ContinuousAt instTopologicalSpaceSubtype	—	Continuous.continuousAt continuous_subtype_val
continuous_apply 📖	mathematical	—	Continuous Pi.topologicalSpace	—	continuous_iInf_dom continuous_induced_dom
continuous_apply_apply 📖	mathematical	—	Continuous Pi.topologicalSpace	—	Continuous.comp continuous_apply
continuous_bool_rng 📖	mathematical	—	Continuous instTopologicalSpaceBool IsClopen Set.preimage Set Set.instSingletonSet	—	continuous_discrete_rng instDiscreteTopologyBool IsClopen.eq_1 isOpen_compl_iff Set.preimage_compl Bool.compl_singleton
continuous_inclusion 📖	mathematical	Set Set.instHasSubset	Continuous Set.Elem instTopologicalSpaceSubtype Set.instMembership Set.inclusion	—	Continuous.subtype_map continuous_id
continuous_map_of_le 📖	mathematical	Setoid.instLE_mathlib	Continuous instTopologicalSpaceQuotient Setoid.map_of_le	—	continuous_coinduced_rng
continuous_map_sInf 📖	mathematical	Set Set.instMembership	Continuous InfSet.sInf Setoid.instInfSet instTopologicalSpaceQuotient Setoid.map_sInf	—	continuous_coinduced_rng
continuous_mulSingle 📖	mathematical	—	Continuous Pi.topologicalSpace Pi.mulSingle	—	Continuous.update continuous_const continuous_id
continuous_ofAdd 📖	mathematical	—	Continuous Multiplicative instTopologicalSpaceMultiplicative DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	continuous_id
continuous_ofDual 📖	mathematical	—	Continuous OrderDual OrderDual.instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual	—	continuous_id
continuous_ofMul 📖	mathematical	—	Continuous Additive instTopologicalSpaceAdditive DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	—	continuous_id
continuous_pi 📖	mathematical	Continuous	Pi.topologicalSpace	—	continuous_pi_iff
continuous_pi_iff 📖	mathematical	—	Continuous Pi.topologicalSpace	—	—
continuous_quot_lift 📖	mathematical	Continuous	instTopologicalSpaceQuot	—	continuous_coinduced_dom
continuous_quot_mk 📖	mathematical	—	Continuous instTopologicalSpaceQuot	—	continuous_coinduced_rng
continuous_quotient_mk' 📖	mathematical	—	Continuous instTopologicalSpaceQuotient	—	continuous_coinduced_rng
continuous_rangeFactorization_iff 📖	mathematical	—	Continuous Set.Elem Set.range instTopologicalSpaceSubtype Set Set.instMembership Set.rangeFactorization	—	Topology.IsInducing.continuous_iff Topology.IsInducing.subtypeVal
continuous_sigma 📖	mathematical	Continuous	instTopologicalSpaceSigma	—	continuous_sigma_iff
continuous_sigmaMk 📖	mathematical	—	Continuous instTopologicalSpaceSigma	—	continuous_iSup_rng continuous_coinduced_rng
continuous_sigma_iff 📖	mathematical	—	Continuous instTopologicalSpaceSigma	—	continuous_iSup_dom continuous_coinduced_dom
continuous_sigma_map 📖	mathematical	—	Continuous instTopologicalSpaceSigma Sigma.map	—	continuous_sigma_iff Topology.IsEmbedding.continuous_iff Topology.IsEmbedding.sigmaMk
continuous_single 📖	mathematical	—	Continuous Pi.topologicalSpace Pi.single	—	Continuous.update continuous_const continuous_id
continuous_subtype_val 📖	mathematical	—	Continuous instTopologicalSpaceSubtype	—	continuous_induced_dom
continuous_toAdd 📖	mathematical	—	Continuous Multiplicative instTopologicalSpaceMultiplicative DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.toAdd	—	continuous_id
continuous_toDual 📖	mathematical	—	Continuous OrderDual OrderDual.instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual	—	continuous_id
continuous_toMul 📖	mathematical	—	Continuous Additive instTopologicalSpaceAdditive DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.toMul	—	continuous_id
continuous_uliftDown 📖	mathematical	—	Continuous ULift.topologicalSpace	—	continuous_induced_dom
continuous_uliftMap 📖	mathematical	Continuous	ULift.topologicalSpace ULift.map	—	Continuous.comp' continuous_uliftUp continuous_uliftDown
continuous_uliftUp 📖	mathematical	—	Continuous ULift.topologicalSpace	—	continuous_induced_rng continuous_id
continuous_update 📖	mathematical	—	Continuous instTopologicalSpaceProd Pi.topologicalSpace Function.update	—	Continuous.update continuous_fst continuous_snd
denseRange_inclusion_iff 📖	mathematical	Set Set.instHasSubset	DenseRange Set.Elem instTopologicalSpaceSubtype Set.instMembership Set.inclusion closure	—	DenseRange.eq_1 Subtype.dense_iff Set.range_comp Set.val_comp_inclusion Subtype.range_coe
exists_finset_piecewise_mem_of_mem_nhds 📖	mathematical	Set Filter Filter.instMembership nhds Pi.topologicalSpace	Set.instMembership Finset.piecewise Finset.decidableMem	—	nhds_pi Finset.piecewise_eq_of_mem Finset.mem_coe mem_of_mem_nhds
exists_open_dense_of_open_dense_subtype 📖	mathematical	Dense IsOpen Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	Set.preimage	—	dense_iff_inter_open Set.nonempty_of_nonempty_preimage IsOpen.preimage_val
frontier_inter_open_inter 📖	mathematical	IsOpen	Set Set.instInter frontier	—	Set.inter_comm IsOpenMap.preimage_frontier_eq_frontier_preimage IsOpen.isOpenMap_subtype_val continuous_subtype_val Subtype.preimage_coe_self_inter
induced_to_pi 📖	mathematical	—	TopologicalSpace.induced Pi.topologicalSpace iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	induced_iInf induced_compose
inducing_iInf_to_pi 📖	mathematical	—	Topology.IsInducing iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice TopologicalSpace.induced Pi.topologicalSpace	—	induced_to_pi
inducing_sigma 📖	mathematical	—	Topology.IsInducing instTopologicalSpaceSigma IsOpen Set Set.instMembership	—	Topology.IsInducing.comp Topology.IsEmbedding.toIsInducing Topology.IsEmbedding.sigmaMk Topology.IsInducing.isOpen_iff isOpen_range_sigmaMk Set.range_sigmaMk Topology.isInducing_iff_nhds Topology.IsInducing.nhds_eq_comap Filter.comap_comap Filter.map_comap_of_mem Filter.mp_mem Filter.preimage_mem_comap IsOpen.mem_nhds Filter.univ_mem'
instCompactSpaceAdditive 📖	mathematical	—	CompactSpace Additive instTopologicalSpaceAdditive	—	—
instCompactSpaceMultiplicative 📖	mathematical	—	CompactSpace Multiplicative instTopologicalSpaceMultiplicative	—	—
instDiscreteTopologyAdditive 📖	mathematical	—	DiscreteTopology Additive instTopologicalSpaceAdditive	—	—
instDiscreteTopologyMultiplicative 📖	mathematical	—	DiscreteTopology Multiplicative instTopologicalSpaceMultiplicative	—	—
instDiscreteTopologySubtype 📖	mathematical	—	DiscreteTopology instTopologicalSpaceSubtype	—	bot_unique isOpen_discrete Set.preimage_image_eq Subtype.val_injective
instDiscreteTopologyULift 📖	mathematical	—	DiscreteTopology ULift.topologicalSpace	—	Topology.IsEmbedding.discreteTopology Topology.IsEmbedding.uliftDown
instLocallyCompactSpaceAdditive 📖	mathematical	—	LocallyCompactSpace Additive instTopologicalSpaceAdditive	—	—
instLocallyCompactSpaceMultiplicative 📖	mathematical	—	LocallyCompactSpace Multiplicative instTopologicalSpaceMultiplicative	—	—
instNoncompactSpaceAdditive 📖	mathematical	—	NoncompactSpace Additive instTopologicalSpaceAdditive	—	—
instNoncompactSpaceMultiplicative 📖	mathematical	—	NoncompactSpace Multiplicative instTopologicalSpaceMultiplicative	—	—
instWeaklyLocallyCompactSpaceAdditive 📖	mathematical	—	WeaklyLocallyCompactSpace Additive instTopologicalSpaceAdditive	—	—
instWeaklyLocallyCompactSpaceMultiplicative 📖	mathematical	—	WeaklyLocallyCompactSpace Multiplicative instTopologicalSpaceMultiplicative	—	—
interior_pi_set 📖	mathematical	—	interior Pi.topologicalSpace Set.pi	—	Set.ext set_pi_mem_nhds_iff
isClosedMap_ofAdd 📖	mathematical	—	IsClosedMap Multiplicative instTopologicalSpaceMultiplicative DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	IsClosedMap.id
isClosedMap_ofDual 📖	mathematical	—	IsClosedMap OrderDual OrderDual.instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual	—	IsClosedMap.id
isClosedMap_ofMul 📖	mathematical	—	IsClosedMap Additive instTopologicalSpaceAdditive DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	—	IsClosedMap.id
isClosedMap_sigmaMk 📖	mathematical	—	IsClosedMap instTopologicalSpaceSigma	—	isClosed_sigma_iff eq_or_ne Set.preimage_image_eq sigma_mk_injective Set.preimage_image_sigmaMk_of_ne isClosed_empty
isClosedMap_toAdd 📖	mathematical	—	IsClosedMap Multiplicative instTopologicalSpaceMultiplicative DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.toAdd	—	IsClosedMap.id
isClosedMap_toDual 📖	mathematical	—	IsClosedMap OrderDual OrderDual.instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual	—	IsClosedMap.id
isClosedMap_toMul 📖	mathematical	—	IsClosedMap Additive instTopologicalSpaceAdditive DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.toMul	—	IsClosedMap.id
isClosed_preimage_val 📖	mathematical	—	IsClosed Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.preimage Set.instHasSubset Set.instInter closure	—	closure_eq_iff_isClosed Topology.IsEmbedding.closure_eq_preimage_closure_image Topology.IsEmbedding.subtypeVal Function.Injective.image_injective Subtype.val_injective Subtype.image_preimage_coe subset_antisymm_iff Set.instReflSubset Set.instAntisymmSubset Set.subset_inter Set.inter_subset_left subset_closure Set.subset_inter_iff
isClosed_range_sigmaMk 📖	mathematical	—	IsClosed instTopologicalSpaceSigma Set.range	—	IsClosedMap.isClosed_range isClosedMap_sigmaMk
isClosed_set_pi 📖	mathematical	IsClosed	Pi.topologicalSpace Set.pi	—	Set.pi_def isClosed_biInter IsClosed.preimage continuous_apply
isClosed_sigma_iff 📖	mathematical	—	IsClosed instTopologicalSpaceSigma Set.preimage	—	—
isDiscrete_iff_discreteTopology 📖	mathematical	—	IsDiscrete DiscreteTopology Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	IsDiscrete.to_subtype
isOpenMap_ofAdd 📖	mathematical	—	IsOpenMap Multiplicative instTopologicalSpaceMultiplicative DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	IsOpenMap.id
isOpenMap_ofDual 📖	mathematical	—	IsOpenMap OrderDual OrderDual.instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual	—	IsOpenMap.id
isOpenMap_ofMul 📖	mathematical	—	IsOpenMap Additive instTopologicalSpaceAdditive DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	—	IsOpenMap.id
isOpenMap_sigma 📖	mathematical	—	IsOpenMap instTopologicalSpaceSigma	—	Sigma.nhds_eq Filter.map_map
isOpenMap_sigmaMk 📖	mathematical	—	IsOpenMap instTopologicalSpaceSigma	—	isOpen_sigma_iff eq_or_ne Set.preimage_image_eq sigma_mk_injective Set.preimage_image_sigmaMk_of_ne isOpen_empty
isOpenMap_sigma_map 📖	mathematical	—	IsOpenMap instTopologicalSpaceSigma Sigma.map	—	isOpenMap_sigma Topology.IsOpenEmbedding.isOpenMap_iff Topology.IsOpenEmbedding.sigmaMk
isOpenMap_toAdd 📖	mathematical	—	IsOpenMap Multiplicative instTopologicalSpaceMultiplicative DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.toAdd	—	IsOpenMap.id
isOpenMap_toDual 📖	mathematical	—	IsOpenMap OrderDual OrderDual.instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual	—	IsOpenMap.id
isOpenMap_toMul 📖	mathematical	—	IsOpenMap Additive instTopologicalSpaceAdditive DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.toMul	—	IsOpenMap.id
isOpen_pi_iff 📖	mathematical	—	IsOpen Pi.topologicalSpace Set Set.instMembership Set.instHasSubset Set.pi SetLike.coe Finset Finset.instSetLike	—	isOpen_iff_nhds nhds_pi Set.eval_image_pi Finset.mem_coe Set.pi_nonempty_iff Set.Subset.trans Set.pi_mono HasSubset.Subset.trans Set.instIsTransSubset Set.eval_image_pi_subset Set.Subset.rfl isOpen_univ Set.mem_univ Set.univ_pi_ite
isOpen_pi_iff' 📖	mathematical	—	IsOpen Pi.topologicalSpace Set Set.instMembership Set.instHasSubset Set.pi Set.univ	—	nonempty_fintype isOpen_iff_nhds nhds_pi HasSubset.Subset.trans Set.instIsTransSubset Set.pi_mono Set.Subset.trans Set.pi_inter_compl Set.inter_subset_left Eq.subset Set.instReflSubset Finset.coe_univ
isOpen_range_sigmaMk 📖	mathematical	—	IsOpen instTopologicalSpaceSigma Set.range	—	IsOpenMap.isOpen_range isOpenMap_sigmaMk
isOpen_set_pi 📖	mathematical	IsOpen	Pi.topologicalSpace Set.pi	—	Set.pi_def Set.Finite.isOpen_biInter IsOpen.preimage continuous_apply
isOpen_sigma_fst_preimage 📖	mathematical	—	IsOpen instTopologicalSpaceSigma Set.preimage	—	Set.biUnion_of_singleton Set.preimage_iUnion₂ Set.iUnion_congr_Prop isOpen_biUnion isOpen_range_sigmaMk
isOpen_sigma_iff 📖	mathematical	—	IsOpen instTopologicalSpaceSigma Set.preimage	—	isOpen_iSup_iff
isQuotientMap_quot_mk 📖	mathematical	—	Topology.IsQuotientMap instTopologicalSpaceQuot	—	—
isQuotientMap_quotient_mk' 📖	mathematical	—	Topology.IsQuotientMap instTopologicalSpaceQuotient	—	—
map_nhds_subtype_coe_eq_nhds 📖	mathematical	Filter.Eventually nhds	Filter.map instTopologicalSpaceSubtype	—	map_nhds_induced_of_mem Subtype.range_val
map_nhds_subtype_val 📖	mathematical	—	Filter.map Set Set.instMembership nhds instTopologicalSpaceSubtype nhdsWithin	—	Topology.IsInducing.map_nhds_eq Topology.IsInducing.subtypeVal Subtype.range_val
mem_nhds_of_pi_mem_nhds 📖	—	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.pi Set.instMembership	—	—	Filter.mem_of_pi_mem_pi nhds_neBot nhds_pi
mem_nhds_subtype 📖	mathematical	—	Set Set.instMembership Filter Filter.instMembership nhds instTopologicalSpaceSubtype Set.instHasSubset Set.preimage	—	mem_nhds_induced
nhdsSet_prod_le 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhdsSet instTopologicalSpaceProd SProd.sprod Set Set.instSProd Filter.instSProd	—	Filter.HasBasis.ge_iff Filter.HasBasis.prod hasBasis_nhdsSet IsOpen.mem_nhdsSet IsOpen.prod Set.prod_mono
nhdsWithin_subtype_eq_bot_iff 📖	mathematical	—	nhdsWithin Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.preimage Bot.bot Filter Filter.instBot Filter.instInf Filter.principal	—	Filter.inf_principal_eq_bot_iff_comap nhdsWithin.eq_1 Filter.comap_inf Filter.comap_principal nhds_induced
nhds_ne_subtype_eq_bot_iff 📖	mathematical	—	nhdsWithin Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Compl.compl Set.instCompl Set.instSingletonSet Bot.bot Filter Filter.instBot Filter.instInf Filter.principal	—	nhdsWithin_subtype_eq_bot_iff Set.preimage_compl Set.image_singleton Function.Injective.preimage_image Subtype.coe_injective
nhds_ne_subtype_neBot_iff 📖	mathematical	—	Filter.NeBot Set.Elem nhdsWithin instTopologicalSpaceSubtype Set Set.instMembership Compl.compl Set.instCompl Set.instSingletonSet Filter Filter.instInf Filter.principal	—	Filter.neBot_iff not_iff_not nhds_ne_subtype_eq_bot_iff
nhds_ofAdd 📖	mathematical	—	nhds Multiplicative instTopologicalSpaceMultiplicative DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd Filter.map	—	—
nhds_ofDual 📖	mathematical	—	nhds DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual Filter.map OrderDual.instTopologicalSpace	—	—
nhds_ofMul 📖	mathematical	—	nhds Additive instTopologicalSpaceAdditive DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul Filter.map	—	—
nhds_pi 📖	mathematical	—	nhds Pi.topologicalSpace Filter.pi	—	nhds_iInf nhds_induced
nhds_subtype 📖	mathematical	—	nhds Set Set.instMembership instTopologicalSpaceSubtype Filter.comap	—	nhds_induced
nhds_subtype_eq_comap 📖	mathematical	—	nhds instTopologicalSpaceSubtype Filter.comap	—	nhds_induced
nhds_subtype_eq_comap_nhdsWithin 📖	mathematical	—	nhds Set Set.instMembership instTopologicalSpaceSubtype Filter.comap nhdsWithin	—	nhds_subtype comap_nhdsWithin_range Subtype.range_val
nhds_toAdd 📖	mathematical	—	nhds DFunLike.coe Equiv Multiplicative EquivLike.toFunLike Equiv.instEquivLike Multiplicative.toAdd Filter.map instTopologicalSpaceMultiplicative	—	—
nhds_toDual 📖	mathematical	—	nhds OrderDual OrderDual.instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual Filter.map	—	—
nhds_toMul 📖	mathematical	—	nhds DFunLike.coe Equiv Additive EquivLike.toFunLike Equiv.instEquivLike Additive.toMul Filter.map instTopologicalSpaceAdditive	—	—
pi_eq_generateFrom 📖	mathematical	—	Pi.topologicalSpace TopologicalSpace.generateFrom setOf Set Finset Set.pi SetLike.coe Finset.instSetLike	—	TopologicalSpace.generateFrom_setOf_isOpen pi_generateFrom_eq
pi_generateFrom_eq 📖	mathematical	—	Pi.topologicalSpace TopologicalSpace.generateFrom setOf Set Finset Set.pi SetLike.coe Finset.instSetLike	—	le_antisymm le_generateFrom isOpen_set_pi Finset.finite_toSet le_iInf coinduced_le_iff_le_induced Function.update_self Finset.coe_singleton Set.singleton_pi
pi_generateFrom_eq_finite 📖	mathematical	Set.sUnion Set.univ	Pi.topologicalSpace TopologicalSpace.generateFrom setOf Set Set.pi	—	nonempty_fintype pi_generateFrom_eq le_antisymm TopologicalSpace.generateFrom_anti Finset.coe_univ le_generateFrom isOpen_iff_forall_mem_open Set.inter_subset_left Set.univ_pi_piecewise Set.piecewise_eq_of_mem Set.piecewise_eq_of_notMem Set.sUnion_eq_univ_iff
set_pi_mem_nhds 📖	mathematical	Set Filter Filter.instMembership nhds	Pi.topologicalSpace Set.pi	—	Set.pi_def Filter.biInter_mem Continuous.continuousAt continuous_apply
set_pi_mem_nhds_iff 📖	mathematical	—	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.pi	—	nhds_pi Filter.pi_mem_pi_iff nhds_neBot
tendsto_pi_nhds 📖	mathematical	—	Filter.Tendsto nhds Pi.topologicalSpace	—	nhds_pi Filter.tendsto_pi
tendsto_subtype_rng 📖	mathematical	—	Filter.Tendsto nhds instTopologicalSpaceSubtype	—	nhds_subtype_eq_comap Filter.tendsto_comap_iff

---

← Back to Index