SumProd

📁 Source: Mathlib/Topology/Constructions/SumProd.lean

Statistics

Metric	Count
Definitions emptySum, prodAssoc, prodComm, prodCongr, prodPUnit, prodProdProdComm, prodSumDistrib, punitProd, sumAssoc, sumComm, sumCongr, sumEmpty, sumProdDistrib, sumSumSumComm, instTopologicalSpaceProd, instTopologicalSpaceSum	16
Theorems along_fst, along_snd, comp₂, comp₃, comp₄, curry_left, curry_right, fst, fst', prodMap, prodMk, prodMk_left, prodMk_right, snd, snd', sumElim, sumMap, uncurry_left, uncurry_right, comp₂, comp₂_of_eq, fst, fst', fst'', prodMap, prodMap', prodMk, snd, snd', snd'', prod, prodMap, curry_nhds, prodMk_nhds, prod_inl_nhds, prod_inr_nhds, prod_nhds, prodMap_nhds, prodMap_nhds, prod_nhds, prod_nhds', fst_nhds, prodMap_nhds, prodMk_nhds, snd_nhds, coe_emptySum, coe_prodComm, coe_prodCongr, coe_punitProd, coe_sumComm, continuous_sumAssoc, continuous_sumAssoc_symm, prodAssoc_toEquiv, prodComm_symm, prodCongr_symm, prodPUnit_apply, prodProdProdComm_symm, sumAssoc_toEquiv, sumComm_symm, sumCongr_refl, sumCongr_symm, sumCongr_trans, sumEmpty_apply, sumProdDistrib_apply, sumProdDistrib_symm_apply, sumSumSumComm_symm, sumSumSumComm_toEquiv, prod, setOf_mapsTo, sumElim, sumElim, sumMap, sumSwap, prod, sumElim, sumSwap, prodMap, sumElim, sumMap, prodMap, instNeBotNhdsWithinIio, instNeBotNhdsWithinIoi, tendsto_iff, prod_mono, inl, inr, inl, inr, prodMap, sumElim, sumElim_left, sumElim_of_separatedNhds, sumElim_right, disjoint_of_sumElim_aux, prodMap, sumElim, sumElim_left, sumElim_of_separatedNhds, sumElim_right, inl, inr, prodMap, isInducing_const_prod, isInducing_prod_const, closure_prod_eq, continuousAt_fst, continuousAt_snd, continuous_curry, continuous_fst, continuous_inf_dom_left₂, continuous_inf_dom_right₂, continuous_inl, continuous_inr, continuous_isLeft, continuous_isRight, continuous_prodMk, continuous_sInf_dom₂, continuous_snd, continuous_sumElim, continuous_sumMap, continuous_sum_dom, continuous_sum_swap, continuous_swap, exists_nhds_square, frontier_prod_eq, frontier_prod_univ_eq, frontier_univ_prod_eq, instDiscreteTopologyProd, interior_prod_eq, isClosedMap_inl, isClosedMap_inr, isClosedMap_sum, isClosedMap_sumElim, isClosedMap_swap, isClosed_range_inl, isClosed_range_inr, isClosed_sum_iff, isEmbedding_graph, isEmbedding_prodMkLeft, isEmbedding_prodMkRight, isEmbedding_sumElim, isInducing_prodMkLeft, isInducing_prodMkRight, isInducing_sumElim, isOpenMap_fst, isOpenMap_inl, isOpenMap_inr, isOpenMap_snd, isOpenMap_sum, isOpenMap_sumElim, isOpen_prod_iff, isOpen_prod_iff', isOpen_range_inl, isOpen_range_inr, isOpen_setOf_disjoint_nhds_nhds, isOpen_sum_iff, isQuotientMap_fst, isQuotientMap_snd, map_fst_nhds, map_fst_nhdsWithin, map_mem_closure₂, map_snd_nhds, map_snd_nhdsWithin, mem_nhdsWithin_prod_iff, mem_nhds_prod_iff, mem_nhds_prod_iff', nhdsWithin_prod_eq, nhds_inl, nhds_inr, nhds_prod_eq, nhds_swap, prod_eq_generateFrom, prod_generateFrom_generateFrom_eq, prod_induced_induced, prod_mem_nhds, prod_mem_nhds_iff	176
Total	192

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
along_fst 📖	—	Continuous instTopologicalSpaceProd	—	—	curry_left
along_snd 📖	—	Continuous instTopologicalSpaceProd	—	—	curry_right
comp₂ 📖	—	Continuous instTopologicalSpaceProd	—	—	comp prodMk
comp₃ 📖	—	Continuous instTopologicalSpaceProd	—	—	comp₂ prodMk
comp₄ 📖	—	Continuous instTopologicalSpaceProd	—	—	comp₃ prodMk
curry_left 📖	—	Continuous instTopologicalSpaceProd	—	—	comp prodMk_left
curry_right 📖	—	Continuous instTopologicalSpaceProd	—	—	comp prodMk_right
fst 📖	—	Continuous instTopologicalSpaceProd	—	—	comp continuous_fst
fst' 📖	mathematical	Continuous	instTopologicalSpaceProd	—	comp continuous_fst
prodMap 📖	mathematical	Continuous	instTopologicalSpaceProd	—	prodMk fst' snd'
prodMk 📖	mathematical	Continuous	instTopologicalSpaceProd	—	continuous_prodMk
prodMk_left 📖	mathematical	—	Continuous instTopologicalSpaceProd	—	prodMk continuous_id' continuous_const
prodMk_right 📖	mathematical	—	Continuous instTopologicalSpaceProd	—	prodMk continuous_const continuous_id'
snd 📖	—	Continuous instTopologicalSpaceProd	—	—	comp continuous_snd
snd' 📖	mathematical	Continuous	instTopologicalSpaceProd	—	comp continuous_snd
sumElim 📖	mathematical	Continuous	instTopologicalSpaceSum	—	continuous_sumElim
sumMap 📖	mathematical	Continuous	instTopologicalSpaceSum	—	continuous_sumMap
uncurry_left 📖	—	Continuous instTopologicalSpaceProd	—	—	comp prodMk_right
uncurry_right 📖	—	Continuous instTopologicalSpaceProd	—	—	comp prodMk_left

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp₂ 📖	—	ContinuousAt instTopologicalSpaceProd	—	—	comp prodMk
comp₂_of_eq 📖	—	ContinuousAt instTopologicalSpaceProd	—	—	comp₂
fst 📖	—	ContinuousAt instTopologicalSpaceProd	—	—	comp continuousAt_fst
fst' 📖	mathematical	ContinuousAt	instTopologicalSpaceProd	—	comp continuousAt_fst
fst'' 📖	mathematical	ContinuousAt	instTopologicalSpaceProd	—	comp continuousAt_fst
prodMap 📖	mathematical	ContinuousAt	instTopologicalSpaceProd	—	prodMk fst'' snd''
prodMap' 📖	mathematical	ContinuousAt	instTopologicalSpaceProd	—	prodMap
prodMk 📖	mathematical	ContinuousAt	instTopologicalSpaceProd	—	Filter.Tendsto.prodMk_nhds
snd 📖	—	ContinuousAt instTopologicalSpaceProd	—	—	comp continuousAt_snd
snd' 📖	mathematical	ContinuousAt	instTopologicalSpaceProd	—	comp continuousAt_snd
snd'' 📖	mathematical	ContinuousAt	instTopologicalSpaceProd	—	comp continuousAt_snd

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod 📖	mathematical	Dense	instTopologicalSpaceProd SProd.sprod Set Set.instSProd	—	closure_prod_eq

DenseRange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prodMap 📖	mathematical	DenseRange	instTopologicalSpaceProd	—	Set.prod_range_range_eq Dense.prod

Filter.Eventually

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
curry_nhds 📖	—	Filter.Eventually nhds instTopologicalSpaceProd	—	—	curry nhds_prod_eq
prodMk_nhds 📖	mathematical	Filter.Eventually nhds	instTopologicalSpaceProd	—	and prod_inl_nhds prod_inr_nhds
prod_inl_nhds 📖	mathematical	Filter.Eventually nhds	instTopologicalSpaceProd	—	continuousAt_fst
prod_inr_nhds 📖	mathematical	Filter.Eventually nhds	instTopologicalSpaceProd	—	continuousAt_snd
prod_nhds 📖	mathematical	Filter.Eventually nhds	instTopologicalSpaceProd	—	prod_mem_nhds

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prodMap_nhds 📖	mathematical	Filter.EventuallyEq nhds	instTopologicalSpaceProd	—	nhds_prod_eq prodMap

Filter.EventuallyLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prodMap_nhds 📖	mathematical	Filter.EventuallyLE nhds	Prod.instLE_mathlib instTopologicalSpaceProd	—	nhds_prod_eq prodMap

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_nhds 📖	mathematical	Filter.HasBasis nhds	instTopologicalSpaceProd SProd.sprod Set Set.instSProd	—	nhds_prod_eq prod
prod_nhds' 📖	mathematical	Filter.HasBasis nhds	instTopologicalSpaceProd SProd.sprod Set Set.instSProd	—	prod_nhds

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fst_nhds 📖	—	Filter.Tendsto nhds instTopologicalSpaceProd	—	—	comp ContinuousAt.tendsto continuousAt_fst
prodMap_nhds 📖	mathematical	Filter.Tendsto nhds	instTopologicalSpaceProd	—	nhds_prod_eq prodMap
prodMk_nhds 📖	mathematical	Filter.Tendsto nhds	instTopologicalSpaceProd	—	nhds_prod_eq prodMk
snd_nhds 📖	—	Filter.Tendsto nhds instTopologicalSpaceProd	—	—	comp ContinuousAt.tendsto continuousAt_snd

Homeomorph

Definitions

Name	Category	Theorems
emptySum 📖	CompOp	1 math math: coe_emptySum
prodAssoc 📖	CompOp	1 math math: prodAssoc_toEquiv
prodComm 📖	CompOp	2 math math: coe_prodComm, prodComm_symm
prodCongr 📖	CompOp	2 math math: coe_prodCongr, prodCongr_symm
prodPUnit 📖	CompOp	1 math math: prodPUnit_apply
prodProdProdComm 📖	CompOp	1 math math: prodProdProdComm_symm
prodSumDistrib 📖	CompOp	—
punitProd 📖	CompOp	1 math math: coe_punitProd
sumAssoc 📖	CompOp	1 math math: sumAssoc_toEquiv
sumComm 📖	CompOp	2 math math: sumComm_symm, coe_sumComm
sumCongr 📖	CompOp	3 math math: sumCongr_refl, sumCongr_symm, sumCongr_trans
sumEmpty 📖	CompOp	1 math math: sumEmpty_apply
sumProdDistrib 📖	CompOp	2 math math: sumProdDistrib_symm_apply, sumProdDistrib_apply
sumSumSumComm 📖	CompOp	2 math math: sumSumSumComm_toEquiv, sumSumSumComm_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_emptySum 📖	mathematical	—	toEquiv instTopologicalSpaceSum emptySum Equiv.emptySum	—	—
coe_prodComm 📖	mathematical	—	DFunLike.coe Homeomorph instTopologicalSpaceProd EquivLike.toFunLike instEquivLike prodComm	—	—
coe_prodCongr 📖	mathematical	—	DFunLike.coe Homeomorph instTopologicalSpaceProd EquivLike.toFunLike instEquivLike prodCongr	—	—
coe_punitProd 📖	mathematical	—	DFunLike.coe Homeomorph instTopologicalSpaceProd instTopologicalSpacePUnit EquivLike.toFunLike instEquivLike punitProd	—	—
coe_sumComm 📖	mathematical	—	DFunLike.coe Homeomorph instTopologicalSpaceSum EquivLike.toFunLike instEquivLike sumComm	—	—
continuous_sumAssoc 📖	mathematical	—	Continuous instTopologicalSpaceSum DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.sumAssoc	—	Continuous.sumElim continuous_inl Continuous.comp' continuous_inr
continuous_sumAssoc_symm 📖	mathematical	—	Continuous instTopologicalSpaceSum DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Equiv.sumAssoc	—	Continuous.sumElim Continuous.comp' continuous_inl continuous_inr
prodAssoc_toEquiv 📖	mathematical	—	toEquiv instTopologicalSpaceProd prodAssoc Equiv.prodAssoc	—	—
prodComm_symm 📖	mathematical	—	symm instTopologicalSpaceProd prodComm	—	—
prodCongr_symm 📖	mathematical	—	symm instTopologicalSpaceProd prodCongr	—	—
prodPUnit_apply 📖	mathematical	—	DFunLike.coe Homeomorph instTopologicalSpaceProd instTopologicalSpacePUnit EquivLike.toFunLike instEquivLike prodPUnit	—	—
prodProdProdComm_symm 📖	mathematical	—	symm instTopologicalSpaceProd prodProdProdComm	—	—
sumAssoc_toEquiv 📖	mathematical	—	toEquiv instTopologicalSpaceSum sumAssoc Equiv.sumAssoc	—	—
sumComm_symm 📖	mathematical	—	symm instTopologicalSpaceSum sumComm	—	—
sumCongr_refl 📖	mathematical	—	sumCongr refl instTopologicalSpaceSum	—	ext
sumCongr_symm 📖	mathematical	—	symm instTopologicalSpaceSum sumCongr	—	—
sumCongr_trans 📖	mathematical	—	trans instTopologicalSpaceSum sumCongr	—	ext
sumEmpty_apply 📖	mathematical	—	DFunLike.coe Homeomorph instTopologicalSpaceSum EquivLike.toFunLike instEquivLike sumEmpty isEmptyElim	—	—
sumProdDistrib_apply 📖	mathematical	—	DFunLike.coe Homeomorph instTopologicalSpaceProd instTopologicalSpaceSum EquivLike.toFunLike instEquivLike sumProdDistrib Equiv Equiv.instEquivLike Equiv.sumProdDistrib	—	—
sumProdDistrib_symm_apply 📖	mathematical	—	DFunLike.coe Homeomorph instTopologicalSpaceSum instTopologicalSpaceProd EquivLike.toFunLike instEquivLike symm sumProdDistrib Equiv Equiv.instEquivLike Equiv.symm Equiv.sumProdDistrib	—	—
sumSumSumComm_symm 📖	mathematical	—	symm instTopologicalSpaceSum sumSumSumComm	—	—
sumSumSumComm_toEquiv 📖	mathematical	—	toEquiv instTopologicalSpaceSum sumSumSumComm Equiv.sumSumSumComm	—	—

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod 📖	mathematical	—	IsClosed instTopologicalSpaceProd SProd.sprod Set Set.instSProd	—	closure_eq_iff_isClosed closure_prod_eq closure_eq
setOf_mapsTo 📖	mathematical	Continuous	IsClosed setOf Set.MapsTo	—	Set.setOf_forall isClosed_biInter preimage

IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sumElim 📖	mathematical	Topology.IsClosedEmbedding	instTopologicalSpaceSum	—	Topology.IsClosedEmbedding.isClosedEmbedding_iff_continuous_injective_isClosedMap Continuous.sumElim IsClosedMap.sumElim

IsClosedMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sumElim 📖	mathematical	IsClosedMap	instTopologicalSpaceSum	—	isClosedMap_sumElim
sumMap 📖	mathematical	IsClosedMap	instTopologicalSpaceSum	—	isClosedMap_sum comp isClosedMap_inl isClosedMap_inr

IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sumSwap 📖	mathematical	—	Topology.IsInducing instTopologicalSpaceSum	—	Topology.IsOpenEmbedding.isInducing IsOpenEmbedding.sumSwap

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod 📖	mathematical	IsOpen	instTopologicalSpaceProd SProd.sprod Set Set.instSProd	—	inter preimage continuous_fst continuous_snd

IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sumElim 📖	mathematical	Topology.IsOpenEmbedding	instTopologicalSpaceSum	—	Topology.isOpenEmbedding_iff_continuous_injective_isOpenMap Continuous.sumElim IsOpenMap.sumElim
sumSwap 📖	mathematical	—	Topology.IsOpenEmbedding instTopologicalSpaceSum	—	Homeomorph.isOpenEmbedding

IsOpenMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prodMap 📖	mathematical	IsOpenMap	instTopologicalSpaceProd	—	isOpenMap_iff_nhds_le nhds_prod_eq Filter.prod_map_map_eq' Filter.prod_mono nhds_le
sumElim 📖	mathematical	IsOpenMap	instTopologicalSpaceSum	—	isOpenMap_sumElim
sumMap 📖	mathematical	IsOpenMap	instTopologicalSpaceSum	—	isOpenMap_sum comp isOpenMap_inl isOpenMap_inr

IsOpenQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prodMap 📖	mathematical	IsOpenQuotientMap	instTopologicalSpaceProd	—	Function.Surjective.prodMap surjective Continuous.prodMap continuous IsOpenMap.prodMap isOpenMap

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNeBotNhdsWithinIio 📖	mathematical	—	Filter.NeBot nhdsWithin instTopologicalSpaceProd Set.Iio instPreorder	—	Filter.NeBot.mono Filter.NeBot.prod nhdsWithin_prod_eq nhdsWithin_mono lt_iff LT.lt.le
instNeBotNhdsWithinIoi 📖	mathematical	—	Filter.NeBot nhdsWithin instTopologicalSpaceProd Set.Ioi instPreorder	—	Filter.NeBot.mono Filter.NeBot.prod nhdsWithin_prod_eq nhdsWithin_mono lt_iff LT.lt.le
tendsto_iff 📖	mathematical	—	Filter.Tendsto nhds instTopologicalSpaceProd	—	nhds_prod_eq Filter.tendsto_prod_iff'

TopologicalSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_mono 📖	mathematical	TopologicalSpace Preorder.toLE PartialOrder.toPreorder instPartialOrder	instTopologicalSpaceProd	—	le_inf LE.le.trans inf_le_left induced_mono inf_le_right

Topology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isInducing_const_prod 📖	mathematical	—	IsInducing instTopologicalSpaceProd	—	induced_inf induced_compose induced_const top_inf_eq
isInducing_prod_const 📖	mathematical	—	IsInducing instTopologicalSpaceProd	—	induced_inf induced_compose induced_const inf_top_eq

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inl 📖	mathematical	—	Topology.IsClosedEmbedding instTopologicalSpaceSum	—	Topology.IsEmbedding.inl isClosed_range_inl
inr 📖	mathematical	—	Topology.IsClosedEmbedding instTopologicalSpaceSum	—	Topology.IsEmbedding.inr isClosed_range_inr

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inl 📖	mathematical	—	Topology.IsEmbedding instTopologicalSpaceSum	—	Topology.IsOpenEmbedding.toIsEmbedding Topology.IsOpenEmbedding.inl
inr 📖	mathematical	—	Topology.IsEmbedding instTopologicalSpaceSum	—	Topology.IsOpenEmbedding.toIsEmbedding Topology.IsOpenEmbedding.inr
prodMap 📖	mathematical	Topology.IsEmbedding	instTopologicalSpaceProd	—	Topology.IsInducing.prodMap isInducing Function.Injective.prodMap injective
sumElim 📖	mathematical	Topology.IsEmbedding Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice closure Set.range	instTopologicalSpaceSum	—	isEmbedding_sumElim
sumElim_left 📖	—	Topology.IsEmbedding instTopologicalSpaceSum	—	—	comp inl
sumElim_of_separatedNhds 📖	mathematical	Topology.IsEmbedding SeparatedNhds Set.range	instTopologicalSpaceSum	—	sumElim SeparatedNhds.disjoint_closure_left SeparatedNhds.disjoint_closure_right
sumElim_right 📖	—	Topology.IsEmbedding instTopologicalSpaceSum	—	—	comp inr

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_of_sumElim_aux 📖	mathematical	Topology.IsInducing instTopologicalSpaceSum	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice closure Set.range	—	isClosed_iff isClosed_range_inl IsClosed.closure_subset_iff Set.range_comp Set.image_subset_iff subset_refl Set.instReflSubset Set.image_univ Set.disjoint_image_right Set.preimage_comp Set.disjoint_image_inl_image_inr Disjoint.mono_left
prodMap 📖	mathematical	Topology.IsInducing	instTopologicalSpaceProd	—	Topology.isInducing_iff_nhds Prod.map_def nhds_prod_eq nhds_eq_comap Filter.prod_comap_comap_eq
sumElim 📖	mathematical	Topology.IsInducing Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice closure Set.range	instTopologicalSpaceSum	—	Topology.isInducing_iff_nhds le_antisymm Filter.Tendsto.le_comap Continuous.tendsto Continuous.sumElim continuous Filter.comap_sumElim_eq nhds_eq_comap nhds_inl Filter.map_eq_bot_iff Filter.comap_eq_bot_iff_compl_range Filter.disjoint_principal_right Disjoint.mono_left nhds_le_nhdsSet Set.mem_range_self disjoint_nhdsSet_principal bot_le nhds_inr Filter.disjoint_principal_left Disjoint.mono_right disjoint_principal_nhdsSet
sumElim_left 📖	—	Topology.IsInducing instTopologicalSpaceSum	—	—	comp Topology.IsEmbedding.isInducing Topology.IsEmbedding.inl
sumElim_of_separatedNhds 📖	mathematical	Topology.IsInducing SeparatedNhds Set.range	instTopologicalSpaceSum	—	sumElim SeparatedNhds.disjoint_closure_left SeparatedNhds.disjoint_closure_right
sumElim_right 📖	—	Topology.IsInducing instTopologicalSpaceSum	—	—	comp Topology.IsEmbedding.isInducing Topology.IsEmbedding.inr

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inl 📖	mathematical	—	Topology.IsOpenEmbedding instTopologicalSpaceSum	—	of_continuous_injective_isOpenMap continuous_inl Sum.inl_injective isOpenMap_inl
inr 📖	mathematical	—	Topology.IsOpenEmbedding instTopologicalSpaceSum	—	of_continuous_injective_isOpenMap continuous_inr Sum.inr_injective isOpenMap_inr
prodMap 📖	mathematical	Topology.IsOpenEmbedding	instTopologicalSpaceProd	—	of_isEmbedding_isOpenMap Topology.IsEmbedding.prodMap toIsEmbedding IsOpenMap.prodMap isOpenMap

(root)

Definitions

Name	Category	Theorems
instTopologicalSpaceProd 📖	CompOp	1365 math math: HasStrictFDerivAt.isBigO_sub, continuous_decomposeProdAdjoint, EReal.continuousAt_add_coe_bot, contMDiff_prod_assoc, NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm, HasStrictFDerivAt.map_implicitFunctionOfComplemented_eq, LowerSemicontinuous.isClosed_epigraph, StarModule.decomposeProdAdjointL_symm_apply, ContinuousMap.HomotopyRel.prod_apply, Trivialization.proj_symm_apply', Real.continuousOn_rpowIntegrand₀₁_uncurry, fderiv_snd, HasStrictFDerivAt.isLittleOTVS, Prod.instLieGroup, instR1SpaceProd, Trivialization.pullback_source, ContinuousAlternatingMap.opNorm_prod, IsSeparatedMap.pullback, TopCat.pullbackIsoProdSubtype_hom_fst, ContinuousAlgHom.coe_fst, NumberField.mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace, CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_snd, EReal.continuousAt_add_coe_top, ContMDiffMul.prod, properSMul_iff, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_fst, ContinuousLinearMap.continuous₂, Homeomorph.finTwoArrow_apply, ContinuousAffineEquiv.prodComm_apply, ContinuousLinearMap.opNorm_prod, ContinuousLinearMap.snd_comp_inr, ContinuousLinearMap.norm_inr_le_one, NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm, prod_mem_nhds, NumberField.mixedEmbedding.measurable_polarCoordReal_symm, isClosedMap_prodMk_right, isOpen_prod_iff, Trivialization.preimageHomeomorph_symm_apply, instCompactIccSpaceProd, IsProperMap.universally_closed, ContinuousMap.HomotopyWith.coe_toContinuousMap, Complex.norm_polarCoord_symm, ContinuousLinearMap.map_add_add, IsBoundedBilinearMap.hasFDerivAt, Manifold.IsImmersionAtOfComplement.target_subset_preimage_target, Trivialization.domExtend_source, MDifferentiableAt.mfderiv_prod, Homeomorph.finTwoArrow_symm_apply, isOpen_lt_prod, Manifold.IsImmersionAt.map_target_subset_target, isClosed_setOf_specializes, prod_nhds_le_of_disjoint_cocompact, ContMDiffOn.prodMk, Real.rpow_eq_nhds_of_neg, norm_jacobiTheta₂_term_fderiv_ge, Complex.integral_comp_pi_polarCoord_symm, ContinuousLinearMap.norm_inl_le_one, instIsTopologicalSemiringProd, ImplicitFunctionData.isInvertible_fderiv_prodFun, intervalIntegral.integral_hasFDerivAt_of_tendsto_ae, IsOpen.trivializationDiscrete_target, NonarchimedeanGroup.Prod.instNonarchimedeanGroup, MeasureTheory.Measure.instIsFiniteMeasureOnCompactsProdVolume, ContinuousLinearEquiv.coe_prodAssoc, MeasureTheory.Measure.instIsLocallyFiniteMeasureProdVolume, ContinuousMap.continuous_prodMk_const, IsHomeomorph.prodMap, mem_nhds_prod_iff, GenLoop.fromLoop_apply, Homeomorph.prodAssoc_toEquiv, continuousOn_prod_of_discrete_right, ContinuousAffineMap.prodMap_apply, TopologicalSpace.NonemptyCompacts.coe_prod, ContinuousAddMonoidHom.snd_toFun, ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl_toLinearEquiv, Trivialization.codExtend_source, intervalIntegral.fderiv_integral_of_tendsto_ae, ContinuousLinearEquiv.snd_equivOfRightInverse, instIsTopologicalAddTorsorProd, DifferentiableAt.prodMap, ImplicitFunctionData.map_pt_mem_toOpenPartialHomeomorph_target, MDifferentiableOn.prodMk_space, ImplicitFunctionData.pt_mem_toPartialHomeomorph_source, SeparationQuotient.isQuotientMap_prodMap_mk, ContinuousWithinAt.continuousLinearMapCoprod, det_fderivPolarCoordSymm, EReal.continuousAt_add_coe_coe, Homeomorph.coe_uniqueProd, ContinuousAlternatingMap.hasStrictFDerivAt_compContinuousLinearMap, MeasureTheory.Measure.toSphere_apply_aux, Manifold.IsImmersionOfComplement.prodMap, NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isComplex, EMetric.NonemptyCompacts.lipschitz_prod, OpenAddSubgroup.toAddSubgroup_prod, ContinuousAddMonoidHom.prodMap_toFun, ContinuousMap.Homotopy.apply_zero_path, ContinuousAffineEquiv.prodCongr_toContinuousAffineMap, HasFDerivWithinAt.prodMap, instDiscreteTopologyProd, chartedSpaceSelf_prod, TopologicalSpace.Compacts.lipschitz_prod, ContinuousAffineEquiv.prodAssoc_toAffineEquiv, ContinuousLinearMap.coprod_comp_prodComm, ContinuousMap.HomotopyWith.prop', ContinuousMultilinearMap.eq_prod_iff, ContinuousLinearMap.coprodEquiv_apply, HasMFDerivWithinAt.prodMk, hasStrictFDerivAt_snd, ContMDiffAdd.prod, uniformity_hasBasis_closed, ContMDiffMul.contMDiff_mul, Continuous.fst', hasStrictFDerivAt_iff_isLittleOTVS, Trivialization.prod_apply, ContinuousVAdd.continuous_vadd, List.Vector.continuous_insertIdx', mdifferentiableOn_snd, Homeomorph.shearAddRight_symm_coe, contMDiff_mul, ContinuousLinearEquiv.prodProdProdComm_symm, isQuotientMap_snd, ContinuousLinearMap.comp_inl_add_comp_inr, WithLp.prodContinuousLinearEquiv_symm_apply, contMDiffWithinAt_snd, ContinuousMap.Homotopy.evalAt_eq, HasFPowerSeriesWithinAt.hasStrictFDerivWithinAt, contMDiffWithinAt_prod_iff, ContinuousLinearMap.coe_snd, ContinuousAddMonoidHom.continuous_comp, FiberPrebundle.continuous_trivChange, ContinuousMultilinearMap.prod_ext_iff, NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume, UniqueMDiffOn.prod, VectorBundleCore.mem_localTriv_target, contMDiff_equivTangentBundleProd_symm, Asymptotics.isLittleOTVS_prodMk_left, NumberField.mixedEmbedding.polarCoordReal_apply, ContinuousAt.fst'', continuousWithinAt_prod_of_discrete_left, Homeomorph.funSplitAt_symm_apply, Homeomorph.shearMulRight_coe, lebesgue_number_of_compact_open, mem_uniformity_isClosed, differentiable_fst, DifferentiableAt.fderiv_prodMk, Real.hasStrictFDerivAt_rpow_of_pos, EReal.continuousAt_add_bot_bot, FiberBundle.prod_trivializationAt', Prod.instIsTopologicalAddGroup, ContinuousAffineMap.prodMap_toAffineMap, Prod.instTietzeExtension, instSigmaCompactSpaceProd, ContinuousMap.exists_finite_sum_mul_approximation_of_mem_uniformity, Trivialization.pullback_target, StarModule.decomposeProdAdjointL_apply, nhdsSet_diagonal_eq_uniformity, FiberPrebundle.continuous_symm_of_mem_pretrivializationAtlas, continuous_prod_of_discrete_right, DifferentiableWithinAt.fderivWithin_prodMk, SeparationQuotient.tendsto_lift₂_nhds, IsOpenMap.prodMap, TopologicalSpace.instFirstCountableTopologyProd, Asymptotics.IsLittleOTVS.prodMk, GenLoop.homotopyTo_apply, LinearMap.IsContPerfPair.bijective_left, prod_induced_induced, Fin.appendHomeomorph_apply, Homeomorph.coe_prodCongr, isProperMap_snd_of_compactSpace, MDifferentiableWithinAt.prodMk_space, Trivialization.contMDiffOn_symm_trans, MeasureTheory.Measure.prod.instIsOpenPosMeasure, Homeomorph.sumArrowHomeomorphProdArrow_apply, Continuous.prodMap, ContinuousLinearMap.coe_equivProdOfSurjectiveOfIsCompl, Trivialization.isImage_preimage_prod, ContinuousAt.fst', NumberField.mixedEmbedding.polarSpaceCoord_target, ContinuousMap.concatCM_left, NumberField.mixedEmbedding.negAt_apply_snd, IsContDiffImplicitAt.hasFDerivAt, Trivialization.eqOn, ImplicitFunctionData.eventuallyEq_implicitFunction, IsClosed.relInv, GroupTopology.continuous_mul', FiberBundleCore.mk_mem_localTrivAt_source, Continuous.snd', ContinuousLinearMap.norm_fst_le, HasStrictFDerivAt.eq_implicitFunctionOfComplemented, hasFDerivAt_snd, mem_nhds_prod_iff', MeasureTheory.AEEqFun.pair_eq_mk, Fin.consEquivL_apply, NumberField.mixedEmbedding.negAt_preimage, ContinuousLinearMap.fst_comp_prod, FiberBundleCore.mem_localTrivAt_source, ContinuousMap.coev_apply, Flow.cont', ContMDiffAdd.contMDiff_add, ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl_apply, Topology.instIsLowerProd, Submodule.coe_orthogonalDecomposition_symm, Trivialization.Prod.continuous_inv_fun, NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne, Manifold.IsSmoothEmbedding.prodMap, NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, continuous_prod_of_continuous_lipschitzWith, Manifold.IsImmersionAtOfComplement.prodMap, Trivialization.coe_coe, TopologicalSpace.IsTopologicalBasis.prod, Trivialization.continuousOn, TopCat.pullbackFst_apply, Diffeomorph.coe_prodCongr, IsCompact.nhdsSetWithin_prod_eq, Manifold.IsImmersionAtOfComplement.map_target_subset_target, Filter.eventually_nhdsSet_prod_iff, MapClusterPt.prodMap, ENNReal.continuousOn_sub, hasMFDerivAt_fst, ImplicitFunctionData.map_pt_mem_toPartialHomeomorph_target, ContinuousAt.prodMap, Complex.hasStrictFDerivAt_cpow', NumberField.mixedEmbedding.negAt_signSet_apply_isComplex, NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure, Prod.totallyDisconnectedSpace, writtenInExtChart_prod, ContinuousLinearMap.opNNNorm_prod, isLocallyInjective_iff_isOpen_diagonal, SeparationQuotient.tendsto_lift₂_nhdsWithin, PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks, ContinuousMap.Homotopy.ulift_apply, MDifferentiableAt.clm_prodMap, Complex.integral_comp_polarCoord_symm, MDifferentiable.prodMap, IsCompact.prod, HasStrictFDerivAt.mem_implicitToPartialHomeomorphOfComplemented_target, cfc_map_prod, continuous_mul, equivTangentBundleProd_apply, contMDiffWithinAt_prod_module_iff, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, NonarchimedeanRing.instProd, TopCat.pullbackSnd_apply, OpenPartialHomeomorph.prod_symm_apply, NumberField.mixedEmbedding.normAtComplexPlaces_polarSpaceCoord_symm, Prod.instNeBotNhdsWithinIio, ContinuousLinearEquiv.uniqueProd_symm_apply, OpenPartialHomeomorph.refl_prod_refl, ContractibleSpace.instProd, VectorBundleCore.localTriv_symm_fst, HasMFDerivWithinAt.prodMap, FiberBundleCore.localTrivAsPartialEquiv_target, MeasureTheory.TendstoInDistribution.prodMk_of_tendstoInMeasure_const, ImplicitFunctionData.pt_mem_toOpenPartialHomeomorph_source, ContinuousLinearEquiv.finTwoArrow_symm_apply, isProperMap_iff_universally_closed, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, ContinuousMonoidHom.swap_toFun, ContinuousAffineEquiv.prodCongr_apply, ContinuousLinearMap.HasLeftInverse.inl, DenseRange.prodMap, FundamentalGroupoidFunctor.prodToProdTop_obj, prod_mem_nhds_iff, frontier_prod_eq, differentiable_snd, MeasureTheory.integrable_prod, ContinuousWithinAt.prodMap, NumberField.mixedEmbedding.convexBodySum_compact, IsModuleTopology.continuous_bilinear_of_pi_fintype, MeasureTheory.charFunDual_prod, ProperSMul.isProperMap_smul_pair, Prod.borelSpace, ContDiff.continuous_fderiv_apply, Complex.equivRealProdCLM_symm_apply, TopologicalSpace.IsCompletelyMetrizableSpace.prod, isEmbedding_prodMkLeft, uniformity_eq_uniformity_closure, Homeomorph.sumProdDistrib_symm_apply, DifferentiableWithinAt.prodMk, LowerSemicontinuousOn.isClosed_re_epigraph, ContinuousAffineEquiv.prodComm_symm_apply, ContinuousAddMonoidHom.inl_toFun, mdifferentiableAt_fst, isOpen_setOf_disjoint_nhds_nhds, Trivialization.target_eq, FundamentalGroupoidFunctor.prodIso_hom, TopCat.pullbackIsoProdSubtype_inv_fst_assoc, OpenSubgroup.coe_prod, lintegral_comp_pi_polarCoord_symm, TopCat.prodIsoProd_hom_snd_assoc, NumberField.mixedEmbedding.fundamentalCone.subset_interior_normLeOne, polarCoord_target, ContinuousMonoidHom.snd_toFun, isSeparatedMap_iff_isClosedEmbedding, CFC.sqrt_map_prod, MDifferentiableOn.prodMk, NumberField.mixedEmbedding.negAt_signSet_apply_isReal, Real.continuousAt_rpow_of_pos, continuous_dist, continuousOn_cfc_setProd, map_fst_nhdsWithin, isEmbedding_graph, MDifferentiableAt.prodMap', Trivialization.restrictPreimage'_source, comp_open_symm_mem_uniformity_sets, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_target, hasFDerivAt_jacobiTheta₂_term, Prod.locallyConvexSpace, continuous_decomposeProdAdjoint_symm, ContMDiffAt.prodMap, hasStrictFDerivAt_iff_isLittleO, HasStrictFDerivAt.prodMk, Bundle.Trivial.isInducing_toProd, Bundle.Trivial.trivialization_target, LocallyFinite.prod_right, IsBoundedBilinearMap.differentiableOn, ContinuousMonoidHom.mul_toFun, mdifferentiableOn_fst, Path.continuous_delayReflRight, ContinuousLinearEquiv.prodCongr_symm, FiberBundle.chartedSpace_chartAt, mdifferentiableOn_prod_module_iff, summable_jacobiTheta₂_term_fderiv_iff, continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith', isInducing_prodMkLeft, Trivialization.symm_apply_eq_mk_continuousLinearEquivAt_symm, nhdset_of_mem_uniformity, TopologicalSpace.Compacts.singleton_prod_singleton, Path.continuous_delayReflLeft, Homeomorph.piSplitAt_symm_apply, ContinuousSup.continuous_sup, Continuous.prodMk_right, uniformity_hasBasis_closure, Prod.instNeBotNhdsWithinIoi, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice, TopologicalSpace.NonemptyCompacts.singleton_prod_singleton, MDifferentiableAt.prodMk, Complex.hasStrictFDerivAt_cpow, ContinuousLinearMap.coe_coprod, Diffeomorph.prodCongr_symm, Manifold.IsImmersionAt.writtenInCharts, TopologicalSpace.NonemptyCompacts.lipschitz_prod, Complex.polarCoord_apply, Homeomorph.sumArrowHomeomorphProdArrow_symm_apply, closure_eq_uniformity, ContinuousMap.Homotopy.apply_one_path, continuous_polarCoord_symm, subset_tangentConeAt_prod_right, mdifferentiable_fst, FiberBundle.Prod.isInducing_diag, RestrictedProduct.continuous_dom_prod, OpenPartialHomeomorph.prod_target, NumberField.mixedEmbedding.polarCoordReal_source, ContinuousLinearMap.coprod_comp_inl_inr, toTopologicalSpace_prod, instPolynormableSpaceProd, Trivialization.domExtend_symm_apply, Real.differentiableAt_rpow_of_ne, subset_tangentConeAt_prod_left, IsOpenQuotientMap.prodMap, Topology.IsEmbedding.prodMap, ContinuousMap.HomotopyLike.toContinuousMapClass, Homeomorph.prodPUnit_apply, MeasureTheory.hasFDerivAt_convolution_right_with_param, mdifferentiableAt_snd, mfderiv_prodMap, TopCat.prodIsoProd_inv_snd_assoc, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, hasFDerivAt_prodMk_left, HasStrictFDerivAt.isLittleO, continuous_edist, interior_prod_eq, ContinuousMultilinearMap.prodEquiv_symm_apply_fst, IsModuleTopology.instProd, HasStrictFDerivAt.map_implicitFunction_eq, FiberPrebundle.totalSpaceMk_isInducing, OrderClosedTopology.isClosed_le', TopCat.prodIsoProd_inv_fst_assoc, HasFDerivWithinAt.inner, Filter.Eventually.prod_nhdsSet, isProperMap_fst_of_compactSpace, ContinuousLinearMap.coprod_add, continuousAt_cpow, Trivialization.prod_symm_apply, instPreconnectedSpaceProd, continuous_snd, continuous_fst, Prod.instBoundedLENhdsClass, ContMDiffWithinAt.prodMk_space, prod_eq_generateFrom, FiberwiseLinear.trans_openPartialHomeomorph_apply, MeasureTheory.memLp_prod_iff, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_apply_ker, ContinuousLinearMap.prod_ext_iff, NumberField.mixedEmbedding.polarCoord_symm_apply, ContinuousMap.uncurry_apply, nhds_prod_le_of_disjoint_cocompact, Homeomorph.piEquivPiSubtypeProd_apply, Filter.Eventually.prod_inl_nhds, HasStrictFDerivAt.implicitToPartialHomeomorph_self, Trivialization.prod.isLinear, measurableSet_pi_polarCoord_target, CommRingCat.HomTopology.isEmbedding_pushout, continuousWithinAt_prod_of_discrete_right, FiberwiseLinear.source_trans_PartialHomeomorph, iSup_nhds_le_uniformity, lowerSemicontinuous_iff_isClosed_epigraph, contMDiff_snd, Prod.continuousInv, contMDiffAt_prod_iff, closure_ball_subset, MDifferentiableOn.clm_prodMap, isClosed_setOf_inseparable, tangentMap_prodSnd, Complex.continuousOn_norm_circleTransformBoundingFunction, FundamentalGroupoidFunctor.projLeft_map, integral_comp_polarCoord_symm, ProperVAdd.isProperMap_vadd_pair, ContinuousAffineEquiv.prodComm_toAffineEquiv, TopologicalSpace.Clopens.finite_prod, differentiable_inner, VectorBundleCore.mem_trivChange_source, HasFDerivWithinAt.prodMk, ContinuousOn.prodMap, LocallyFinite.prod_left, continuous_sup, ContMDiffAt.prodMk_space, HasMFDerivAt.prodMap, ContinuousLinearMap.fpowerSeriesBilinear_apply_add_three, hasSum_jacobiTheta₂_term_fderiv, MeasureTheory.MemLp.of_fst_snd, FiberBundle.writtenInExtChartAt_trivializationAt, Prod.tendsto_iff, map_snd_nhdsWithin, isSeparatedMap_iff_isClosedMap, ContinuousMultilinearMap.prodL_apply, ContinuousMap.prodMap_apply, OpenPartialHomeomorph.prod_apply, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, Filter.Eventually.prod_inr_nhds, frontier_prod_univ_eq, NumberField.mixedEmbedding.negAt_apply_isReal_and_notMem, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_source, Submodule.coe_orthogonalDecomposition, hasMFDerivWithinAt_fst, differentiableAt_fst, isLocallyInjective_iff_isOpenMap, QuotientRing.isQuotientMap_coe_coe, ContinuousLinearMap.coe_inr, continuousOn_prod_of_continuousOn_lipschitzOnWith, lowerSemicontinuousOn_iff_isClosed_epigraph, NNReal.continuousAt_rpow, ContinuousLinearEquiv.prodComm_apply, AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback, IsBoundedBilinearMap.continuous, continuous_min, continuous_swap, isCompact_diagonal, ContinuousLinearEquiv.coe_prodCongr, intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae, NumberField.mixedEmbedding.volume_preserving_negAt, MDifferentiableOn.prodMap, TopologicalSpace.metrizableSpace_prod, mdifferentiableAt_prod_module_iff, OpenPartialHomeomorph.prod_symm, isOpenMap_prod_of_discrete_right, HasFPowerSeriesAt.isBigO_image_sub_norm_mul_norm_sub, NumberField.mixedEmbedding.negAt_apply_isComplex, Complex.hasFDerivAt_cpow, ContinuousMap.prodSwap_apply, Prod.noncompactSpace_iff, Trivialization.preimage_subset_source, Trivialization.proj_surjOn_baseSet, WithLp.prodContinuousLinearEquiv_symm_apply_ofLp, ENat.continuousAt_sub, ContinuousLinearEquiv.finTwoArrow_apply, compactSpace_uniformity, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_target, ENNReal.tendsto_mul, Stonean.extremallyDisconnected_pullback, ImplicitFunctionData.toPartialHomeomorph_coe, FiberBundleCore.mem_localTriv_source, Topology.IsEmbedding.toPullbackDiag, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_self, IsPicardLindelof.continuousOn_uncurry, continuousOn_div, GenLoop.toLoop_apply, NumberField.mixedEmbedding.normAtComplexPlaces_normAtAllPlaces, CFC.rpow_map_prod, Bundle.Trivial.homeomorphProd_symm_apply_snd, IsBoundedBilinearMap.isBoundedLinearMap_deriv, ContinuousLinearMap.prodMapL_apply, MDifferentiable.prodMk_space, contMDiff_smul, VectorBundleCore.mem_source_at, intervalIntegral.integral_hasStrictFDerivAt, prodChartedSpace_chartAt, NumberField.mixedEmbedding.mem_negAt_plusPart_of_mem, instCompletelyRegularSpaceProd, ContinuousLinearMap.continuousMultilinearMapOption_apply_eq_self, EReal.continuousAt_add_bot_coe, instParacompactSpaceProdOfCompactSpace, IsBoundedBilinearMap.differentiableAt, Prod.continuousConstSMul, Filter.coprod_cocompact, Trivialization.mem_target, ContinuousAt.prodMap', ContinuousLinearMap.comp_coprod, Continuous.continuousLinearMapCoprod, NumberField.mixedEmbedding.fundamentalCone.closure_normLeOne_subset, HSpace.hmul_e_e, ContinuousLinearMap.uncurryBilinear_apply, OpenPartialHomeomorph.prod_toPartialEquiv, nhdsSet_diagonal_le_uniformity, TopologicalSpace.Compacts.coe_prod, IsBoundedBilinearMap.hasFDerivWithinAt, FiberBundle.chartedSpace'_chartAt, MDifferentiableWithinAt.prodMk, NumberField.mixedEmbedding.convexBodySumFun_continuous, CommRingCat.HomTopology.mvPolynomialHomeomorph_symm_apply_hom, FiberBundleCore.mem_localTrivAt_target, nhdsKer_pair, ContinuousAlgHom.coe_prod, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, ContinuousMultilinearMap.smul_prod_smul, Filter.Germ.sliceRight_coe, ContinuousMultilinearMap.prodEquiv_symm_apply, TangentBundle.trivializationAt_source, Trivialization.coe_mem_source, Diffeomorph.coe_prodComm, Units.isEmbedding_embedProduct, IsClosed.epigraph, ContinuousDiv.continuous_div', polarCoord_symm_apply, Trivialization.codExtend'_target, isClosed_diagonal, ContinuousLinearMap.continuousWithinAt_uncurry_of_multilinear, NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm, ContinuousAddMonoidHom.prod_toFun, ContMDiffOn.prodMk_space, isProperMap_iff_isClosedMap_ultrafilter, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, TopCat.pullbackIsoProdSubtype_inv_snd_apply, FiberPrebundle.isOpen_target_of_mem_pretrivializationAtlas_inter, ContinuousLinearMap.norm_inr, ImplicitFunctionData.implicitFunction_apply, ContinuousAffineMap.prod_contLinear, nhds_swap, homeomorphUnitSphereProd_symm_apply_coe, unitInterval.continuous_qRight, ContinuousAddMonoidHom.coprod_toFun, TopologicalSpace.Clopens.exists_finset_eq_sup_prod, nhds_le_uniformity, ProbabilityTheory.indepFun_iff_charFunDual_prod', IsModuleTopology.continuous_bilinear_of_finite_left, ContinuousMul.continuous_mul, Asymptotics.IsBigOTVS.prodMk, Prod.noncompactSpace_left, TopologicalSpace.CompactOpens.coe_prod, equivTangentBundleProd_symm_apply_snd, Topology.continuous_reorderRestrictProd, TopCat.pullbackIsoProdSubtype_inv_fst, ContinuousOn.prod_mapL, TangentBundle.chartAt, ContinuousAlternatingMap.prod_apply, continuous_inf, t2_iff_isClosed_diagonal, Path.trans_prod_eq_prod_trans, Path.Homotopy.continuous_reflTransSymmAux, Module.Basis.prod_parallelepiped, ContinuousMap.Homotopic.prodMap, ContinuousAt.continuousLinearMapCoprod, FiberBundleCore.mem_localTriv_target, Filter.EventuallyLE.prodMap_nhds, ContinuousAffineMap.prodMap_contLinear, List.continuous_insertIdx, ContMDiffOn.prodMap, hasFDerivAtFilter_snd, continuousAt_prod_of_discrete_right, ContMDiffRing.contMDiff_mul, TopologicalSpace.Closeds.continuous_infEDist, contMDiff_prod_iff, Trivialization.mem_source, FiberBundle.extChartAt, Path.continuous_uncurry_iff, WithLp.prod_continuous_toLp, ContinuousLinearEquiv.coe_prodProdProdComm, HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented_self, Orientation.continuousAt_oangle, Trivialization.symm_apply, SeparationQuotient.continuousAt_lift₂, ContDiffOn.continuousOn_fderivWithin_apply, Fin.appendHomeomorph_toEquiv, Complex.lintegral_comp_polarCoord_symm, ImplicitFunctionData.hasStrictFDerivAt, ContinuousLinearMap.coprodEquivL_apply_apply, mfderiv_prod_right, Trivialization.source_inter_preimage_target_inter, MDifferentiable.clm_prodMap, ContinuousLinearEquiv.skewProd_apply, Complex.continuousAt_ofReal_cpow, IsCompact.nhdsSet_prod_eq, EuclideanGeometry.continuousAt_angle, Path.prod_coe, instCompactSpaceProd, Prod.continuousAdd, isHomeomorphicTrivialFiberBundle_snd, NumberField.mixedEmbedding.polarCoord_source, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, Differentiable.prodMk, MeasureTheory.AEStronglyMeasurable.prodMk, HasFDerivAtFilter.prodMk, TopCat.prodIsoProd_hom_snd, MeasureTheory.Measure.prod.instIsLocallyFiniteMeasure, DifferentiableAt.prodMk, Topology.image_snd_preimageImageRestrict, MeasureTheory.integral_continuousLinearMap_prod, Real.continuousAt_rpow_of_ne, HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented_fst, NumberField.mixedEmbedding.continuous_norm, ContinuousMultilinearMap.prodEquiv_apply, ModelWithCorners.boundary_of_boundaryless_left, ContinuousLinearMap.HasLeftInverse.prodMap, TopCat.pullbackIsoProdSubtype_hom_snd, AddGroupTopology.continuous_add', IsClosed.hypograph, UniformOnFun.continuousOn_eval₂, UniformSpace.Completion.denseRange_coe₃, Complex.continuousAt_cpow_zero_of_re_pos, NumberField.mixedEmbedding.polarSpaceCoord_symm_apply, Complex.measurableEquivRealProd_symm_polarCoord_symm_apply, instParacompactSpaceProdOfCompactSpace_1, Homeomorph.Set.prod_apply, cfcₙ_map_prod, NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces, ProbabilityTheory.IsGaussian.map_rotation_eq_self, continuous_inner, homeomorphSphereProd_symm_apply_coe, ContinuousLinearEquiv.prodUnique_symm_apply, continuousOn_snd, EuclideanGeometry.continuousAt_oangle, FiberBundle.prod_trivializationAtlas', tendsto_sub_comap_self, hasFDerivAtFilter_fst, MDifferentiableAt.prodMk_space, Homeomorph.sumProdDistrib_apply, HasFDerivAt.inner, MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd, TopCat.pullbackIsoProdSubtype_inv_snd, ContinuousMultilinearMap.prodEquiv_symm_apply_snd, Prod.noncompactSpace_right, instWeaklyLocallyCompactSpaceProd, nhdsKer_prod, homeomorphUnitSphereProd_apply_fst_coe, Homeomorph.prodUnique_symm_apply_snd, ContinuousMap.continuous_coev, TopCat.prodIsoProd_inv_fst, HasStrictFDerivAt.isEquivalent_sub, ContinuousLinearMap.continuous_uncurry_of_multilinear, hasFDerivAt_polarCoord_symm, ContinuousLinearMap.inr_apply, Trivialization.proj_clift, ContinuousLinearEquiv.uniqueProd_apply, NumberField.mixedEmbedding.mixedSpaceToRealMixedSpace_apply, properVAdd_iff, Continuous.prod_map_equivL, Homeomorph.shearMulRight_symm_coe, continuous_prod_of_discrete_left, continuousOn_fst, FiberwiseLinear.target_trans_openPartialHomeomorph, GenLoop.toLoop_apply_coe, nhdsSet_prod_le_of_disjoint_cocompact, ContinuousSub.continuous_sub, IsClosed.prod, IsBoundedBilinearMap.fderiv, ContinuousMap.continuous_uncurry, ContinuousMap.curry_apply, mdifferentiable_snd, OpenPartialHomeomorph.prod_symm_trans_prod, Prod.instT0Space, instInfConvergenceClassProd, NumberField.mixedEmbedding.polarCoord_target, uniformity_hasBasis_open_symmetric, mdifferentiableAt_prod_iff, MDifferentiable.prodMk, OpenPartialHomeomorph.extend_prod, NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isReal, contMDiffWithinAt_fst, IsContDiffImplicitAt.bijective, ContMDiffFiberwiseLinear.hasGroupoid, ContinuousMultilinearMap.opNNNorm_prod, ContinuousAlgHom.coe_prodMap, ProperVAdd.isProperMap_vadd_pair_set, ContMDiffWithinAt.prodMk, ContinuousLinearMap.snd_comp_prod, ContinuousMap.image_coev, isOpenMap_fst, IsHomeomorphicTrivialFiberBundle.proj_eq, NumberField.mixedEmbedding.negAt_symm, IsContDiffImplicitAt.eventually_implicitFunction_apply_eq, ProbabilityTheory.IsKolmogorovProcess.measurablePair, Trivialization.symm_trans_target_eq, contMDiffOn_fst, Complex.polarCoord_source, MeasureTheory.Measure.prod.instIsAddHaarMeasure, isClosedMap_swap, nhdsWithin_prod, MeasureTheory.SimpleFunc.integrable_pair, ContinuousLinearMap.ker_prod, NumberField.mixedEmbedding.polarCoord_symm_eq, uniformity_eq_uniformity_interior, Prod.t2Space, Complex.continuousOn_prod_circle_transform_function, Homeomorph.Set.prod_symm_apply_coe, contMDiffOn_prod_iff, continuous_update, Trivialization.pullback_symm_apply_snd, NumberField.mixedEmbedding.negAt_apply_isReal_and_mem, hasFDerivAt_jacobiTheta₂, tendsto_mul_cocompact_nhds_zero, NumberField.mixedEmbedding.polarSpaceCoord_target', VectorPrebundle.totalSpaceMk_isInducing, TopCat.pullbackIsoProdSubtype_inv_fst_apply, ContinuousLinearMap.fst_comp_inl, NumberField.mixedEmbedding.volume_negAt_plusPart, ContinuousLinearEquiv.prodAssoc_apply, Prod.locallyCompactSpace, Trivialization.prod_symm_apply_proj, Bundle.Trivial.toOpenPartialHomeomorph_trivialization_symm_apply, ContinuousLinearMap.fst_comp_inr, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_prodMk, Trivialization.prod_symm_apply_snd, Manifold.IsImmersionAt.prodMap, IsManifold.prod, IsOpen.trivializationDiscrete_source, IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn, specializes_prod, Pretrivialization.open_target, Prod.fst_exp, Filter.HasBasis.uniformity_closure, mfderivWithin_prodMap, instStronglyLocallyContractibleSpaceProd, hasStrictFDerivAt_fst, Trivialization.restrictPreimage'_target, NumberField.mixedEmbedding.iUnion_negAt_plusPart_union, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal, SmoothBumpCovering.embeddingPiTangent_injOn, FiberBundleCore.localTrivAsPartialEquiv_source, Trivialization.symm_coe_proj, Filter.HasBasis.prod_nhds, ContinuousLinearEquiv.prodComm_symm, ContinuousLinearEquiv.coe_uniqueProd, ContinuousAlgHom.coe_fst', IsTopologicalAddTorsor.continuous_vsub, Specializes.prod, Filter.Eventually.prodMk_nhds, Manifold.IsImmersion.prodMap, IsBoundedBilinearMap.hasStrictFDerivAt, ProbabilityTheory.HasGaussianLaw.prodMk, mfderiv_snd, Homeomorph.uniqueProd_symm_apply_snd, ContinuousLinearEquiv.prodAssoc_toLinearEquiv, ContMDiffAt.clm_prodMap, Path.subpathAux_continuous, NumberField.mixedEmbedding.continuous_normAtPlace, nhdsSet_prod_le, Homeomorph.coe_prodComm, Prod.continuousSMul, mem_nhdsWithin_prod_iff, Homeomorph.piFinTwo_apply, EReal.continuousAt_add_top_coe, isQuotientMap_fst, IsProperMap.prodMap, GromovHausdorff.HD_below_aux2, Trivialization.Prod.continuous_to_fun, ContinuousAt.snd', MeasureTheory.ProbabilityMeasure.continuous_prod, intervalIntegral.continuousAt_parametric_primitive_of_dominated, IsDenseEmbedding.prodMap, map_snd_nhds, instMemTrivializationAtlasProdProd, ContinuousLinearEquiv.prodProdProdComm_toLinearEquiv, ContinuousLinearMap.rotation_apply, ContinuousLinearMap.continuousOn_uncurry_of_multilinear, Homeomorph.sigmaProdDistrib_symm_apply, HasFPowerSeriesWithinAt.isBigO_image_sub_norm_mul_norm_sub, NumberField.mixedEmbedding.injective_mixedSpaceOfRealSpace, ContinuousMap.continuous_uncurry_of_continuous, hom_trivializationAt_source, HasStrictFDerivAt.implicitToOpenPartialHomeomorph_self, TopologicalSpace.Clopens.surjective_finset_sup_prod, Topology.IsInducing.prodMap, NumberField.mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace, continuous_algebraMap_iff_smul, ContinuousAddMonoidHom.fst_toFun, ContinuousAffineEquiv.prodCongr_symm, instConnectedSpaceProd, SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, Trivialization.domExtend_target, Trivialization.prod_target, HasSum.prodMk, MapClusterPt.curry_prodMap, LinearMap.IsContPerfPair.bijective_right, FiberBundle.mem_trivializationAt_proj_source, inducing_pullbackTotalSpaceEmbedding, intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae, continuous_prod_of_dense_continuous_lipschitzWith', tendsto_div_comap_self, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, tendsto_add, ENNReal.tendsto_sub, continuousOn_prod_of_continuousOn_lipschitzOnWith', HasStrictFDerivAt.implicitToOpenPartialHomeomorph_fst, ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap, mdifferentiableWithinAt_snd, ContinuousAlgHom.prodEquiv_apply, Topology.IsQuotientMap.trivializationOfVAddDisjoint_source, mfderiv_prodMk, instR0SpaceProd, ContinuousMap.Homotopy.continuous, hasMFDerivWithinAt_snd, contMDiff_prod_module_iff, Homeomorph.coe_prodUnique, HasStrictFDerivAt.implicitToOpenPartialHomeomorph_apply_ker, ContinuousMonoidHom.diag_toFun, HasProd.prodMk, isClosedMap_prodMk_left, ContinuousLinearMap.norm_fst, IsLocallyInjective_iff_isOpenEmbedding, TopologicalSpace.instSeparableSpaceProd, Topology.instIsUpperProd, TopCat.pullbackIsoProdSubtype_hom_apply, intervalIntegral.fderivWithin_integral_of_tendsto_ae, Path.continuous_trans, isInducing_prodMkRight, HasStrictFDerivAt.isBigOTVS_sub, Bundle.Trivial.homeomorphProd_symm_apply_proj, FiberBundle.writtenInExtChartAt_trivializationAt_symm, ModelWithCorners.boundary_of_boundaryless_right, continuousAt_jacobiTheta₂, HasFDerivAt.prodMk, TopologicalSpace.prod_mono, FiberwiseLinear.target_trans_PartialHomeomorph, Manifold.IsImmersionAt.target_subset_preimage_target, isProperMap_iff_isClosedMap_filter, Trivialization.preimageHomeomorph_apply, isOpenMap_snd, Trivialization.apply_symm_apply', ContinuousLinearMap.hasFDerivAt_uncurry_of_multilinear, hasFDerivWithinAt_fst, ContMDiff.clm_prodMap, ContinuousMap.exists_finite_sum_smul_approximation_of_mem_uniformity, intervalIntegral.integral_hasFDerivWithinAt, MeasureTheory.StronglyMeasurable.prodMk, SmoothBumpCovering.embeddingPiTangent_injective, MeasureTheory.charFunDual_prod', Trivialization.restrictPreimage_source, IsBoundedBilinearMap.deriv_apply, HasStrictFDerivAt.isThetaTVS_sub, ContinuousLinearMap.range_eq_map_coprodSubtypeLEquivOfIsCompl, ContinuousLinearEquiv.skewProd_symm_apply, Trivialization.mk_coordChange, IsManifold.mem_maximalAtlas_prod, Trivialization.prod_baseSet, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex, ContinuousMap.Homotopy.coe_toContinuousMap, Trivialization.preimageSingletonHomeomorph_symm_apply, contMDiff_equivTangentBundleProd, HasStrictFDerivAt.prodMap, ContinuousLinearMap.HasRightInverse.prodMap, ContinuousAt.snd'', HasDerivAtFilter.prodMk, LinearPMap.closure_def, ContinuousMultilinearMap.prodL_symm_apply, continuous_add, ContinuousLinearMap.norm_inl, NumberField.mixedEmbedding.lintegral_comp_polarCoordReal_symm, tendsto_mul, Path.subpath_continuous_family, Trivialization.mk_symm, NumberField.mixedEmbedding.measurable_polarCoord_symm, continuousAt_prod_of_discrete_left, MeasureTheory.Measure.prod.instIsHaarMeasure, HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented_apply, Homeomorph.piEquivPiSubtypeProd_symm_apply, Matrix.toLin_finTwoProd_toContinuousLinearMap, Topology.IsQuotientMap.trivializationOfSMulDisjoint_target, instContinuousStarProd, Trivialization.continuousOn_proj, instIsAddHaarMeasureProdRealVolume, Units.isClosedEmbedding_embedProduct, HasStrictDerivAt.prodMk, det_fderivPiPolarCoordSymm, TopCat.prodIsoProd_hom_apply, injOn_pi_polarCoord_symm, ModelWithCorners.boundary_prod, nhdsWithin_prod_eq, ContinuousOn.prodMk, NumberField.mixedEmbedding.polarCoord_apply, NumberField.mixedEmbedding.hasFDerivAt_polarCoordReal_symm, ContinuousMap.Homotopy.prod_apply, ContinuousLinearMap.prodL_apply, equivTangentBundleProd_eq_tangentMap_prod_tangentMap, Complex.equivRealProdCLM_symm_apply_re, ContinuousMonoidHom.inl_toFun, MeasureTheory.Integrable.prodMk, NumberField.mixedEmbedding.continuous_normAtAllPlaces, EReal.lowerSemicontinuous_add, TopCat.pullbackIsoProdSubtype_inv_snd_assoc, TopCat.prodIsoProd_hom_fst, continuous_prodMk, FundamentalGroupoidFunctor.prodIso_inv, HasDerivAt.prodMk, ContinuousLinearMap.coprod_apply, mdifferentiable_prod_iff, ContinuousLinearMap.coe_fst', ContinuousAlgHom.coe_prodMap', hasFDerivAt_pi_polarCoord_symm, Homeomorph.shearAddRight_coe, mdifferentiableOn_prod_iff, BoundedContinuousFunction.continuous_eval, ContinuousAddMonoidHom.diag_toFun, Filter.EventuallyEq.prodMap_nhds, continuous_prod_of_dense_continuous_lipschitzWith, ContinuousLinearEquiv.prodUnique_apply, mfderivWithin_prodMk, Trivialization.pullback_symm_apply_proj, Prod.continuousConstVAdd, UpperSemicontinuous.IsClosed_hypograph, contMDiffAt_prod_module_iff, ContinuousMap.continuous_comp', continuousOn_prod_of_discrete_left, continuousWithinAt_snd, lintegral_comp_polarCoord_symm, HasStrictFDerivAt.mem_implicitToPartialHomeomorphOfComplemented_source, Filter.Germ.sliceLeft_coe, ContinuousAlternatingMap.prodLIE_apply, Manifold.IsImmersionAtOfComplement.writtenInCharts, polarCoord_apply, isOpen_iff_isOpen_ball_subset, ContinuousMap.Homotopy.map_one_left, ContMDiffAt.prodMap', AffineMap.lineMap_continuous_uncurry, RestrictedProduct.continuous_dom_prod_right, Topology.isInducing_const_prod, NumberField.mixedEmbedding.normAtPlace_negAt, ContinuousLinearMap.coprod_comp_inr, Prod.continuousVAdd, HasDerivWithinAt.prodMk, ContinuousLinearMap.coe_snd', FundamentalGroupoidFunctor.projRight_map, ProbabilityTheory.IndepFun.hasGaussianLaw, t2Space_iff_of_isOpenQuotientMap, tangentMap_prodFst, ContinuousMap.Homotopic.prodMk, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply, ContinuousLinearMap.HasLeftInverse.inr, inseparable_iff_clusterPt_uniformity, MeasureTheory.Measure.prod.instIsFiniteMeasureOnCompacts, TopologicalSpace.IsCompletelyPseudoMetrizableSpace.prod, inseparable_prod, Units.continuous_embedProduct, ContinuousAddMonoidHom.add_toFun, TopCat.prodIsoProd_inv_snd, Trivialization.sourceHomeomorphBaseSetProd_symm_apply, ImplicitFunctionData.right_map_implicitFunction, EReal.continuousAt_add, Path.truncate_const_continuous_family, WithLp.toEquiv_homeomorphProd, NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ, Prod.instIsTopologicalGroup, continuousOn_cfcₙ_setProd, ContinuousLinearMap.coe_prodMap', TopologicalSpace.Clopens.countable_prod, Prod.supConvergenceClass, prod_generateFrom_generateFrom_eq, Inseparable.nhds_le_uniformity, IsConnected.prod, upperSemicontinuous_iff_IsClosed_hypograph, Trivialization.symm_trans_source_eq, ContinuousLinearMap.prodEquiv_apply, NumberField.mixedEmbedding.polarSpaceCoord_apply, Submodule.ClosedComplemented.exists_submodule_equiv_prod, differentiableWithinAt_snd, ContMDiffWithinAt.prodMap', polarCoord_source_ae_eq_univ, mdifferentiableWithinAt_fst, NumberField.mixedEmbedding.negAt_apply_norm_isReal, nhds_prod_eq, ContinuousMultilinearMap.neg_prod_neg, CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_fst, closure_eq_inter_uniformity, VectorBundleCore.mem_localTriv_source, IsTopologicalGroup.continuous_conj_prod, isClosedMap_snd_of_compactSpace, ModelWithCorners.BoundarylessManifold.prod, ContinuousLinearMap.snd_comp_inl, homeomorphSphereProd_apply_snd_coe, cpow_eq_nhds', differentiableAt_snd, ContinuousMap.fst_apply, Real.rpow_eq_nhds_of_pos, ContinuousMonoidHom.inr_toFun, ContinuousLinearMap.fst_prod_snd, PrimeSpectrum.continuous_tensorProductTo, TopologicalSpace.IsSeparable.prod, ContinuousSMul.continuous_smul, UniformSpace.Completion.denseRange_coe₂, ContinuousMap.concatCM_right, contMDiff_add, Filter.Eventually.prod_nhds, SeparationQuotient.continuousWithinAt_lift₂, HasStrictFDerivAt.isTheta_sub, Real.continuousAt_rpow, EReal.continuousAt_add_top_top, IsDenseInducing.prodMap, ProperSMul.isProperMap_smul_pair_set, ContinuousAffineEquiv.prodComm_symm, ContinuousLinearMap.inl_apply, Path.truncate_continuous_family, ContinuousEval.continuous_eval, Diffeomorph.prodComm_symm, ContinuousLinearMap.HasRightInverse.snd, Prod.instLieAddGroup, HasMFDerivAt.prodMk, CStarModule.continuous_inner, Trivialization.mk_mem_target, ContinuousAffineMap.prod_apply, interior_mem_uniformity, ContinuousLinearEquiv.prodProdProdComm_apply, ContinuousAddMonoidHom.inr_toFun, TopologicalSpace.pseudoMetrizableSpace_prod, Homeomorph.prodProdProdComm_symm, TopCat.prodIsoProd_hom_fst_assoc, ContinuousInf.continuous_inf, MeasureTheory.integrable_continuousLinearMap_prod, ContinuousAlgHom.fst_comp_prod, Trivialization.contMDiffOn_symm, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply_snd, TopologicalSpace.PositiveCompacts.coe_prod, Fin.appendHomeomorph_symm_apply, continuousAt_jacobiTheta₂', ContinuousLinearEquiv.coe_prodUnique, List.continuous_cons, ContinuousMonoidHom.coprod_toFun, IsContDiffImplicitAt.comp_implicitFunctionAux_eq_snd, OpenPartialHomeomorph.prod_source, ContinuousLinearMap.coe_fst, ImplicitFunctionData.toOpenPartialHomeomorph_coe, continuousWithinAt_prod_iff, ContinuousMap.HomotopyWith.continuous, CFC.nnrpow_eq_nnrpow_prod, ContMDiffAt.prodMk, NumberField.mixedEmbedding.polarSpaceCoord_source, map_fst_nhds, homeomorphUnitSphereProd_apply_snd_coe, ProbabilityTheory.variance_dual_prod, FiberBundleCore.continuousOn_coordChange, Trivialization.codExtend_target, Complex.lintegral_comp_pi_polarCoord_symm, ContinuousLinearMap.coe_inl, ContMDiffWithinAt.clm_prodMap, ImplicitFunctionData.prod_map_implicitFunction, Complex.equivRealProdCLM_symm_apply_im, Complex.polarCoord_symm_apply, Path.Homotopic.prod_lift, prod_le_borel_prod, ContinuousAffineEquiv.prodAssoc_apply, Topology.IsQuotientMap.trivializationOfSMulDisjoint_source, UniformOnFun.continuousAt_eval₂, instIsTopologicalRingProd, Cube.insertAt_boundary, ContinuousAffineEquiv.prodCongr_toAffineEquiv, mdifferentiableWithinAt_prod_module_iff, Action.isContinuous_def, hasMFDerivAt_snd, ContinuousAlgHom.fst_prod_snd, NumberField.mixedEmbedding.polarCoord_target_eq_polarCoordReal_target, instT35SpaceProd, homeomorphSphereProd_apply_fst_coe, isOpen_prod_iff', nhds_eq_uniformity_prod, ContinuousLinearMap.range_prod_eq, MeasureTheory.AEEqFun.pair_mk_mk, Trivialization.apply_symm_apply_eq_coordChangeL, Prod.continuousNeg, EReal.tendsto_mul, MDifferentiableWithinAt.prodMap, MeasureTheory.Lp.compMeasurePreserving_continuous, fderiv_fst, NumberField.mixedEmbedding.instIsAddHaarMeasureRealMixedSpaceVolume, ContinuousMonoidHom.prod_toFun, jacobiTheta₂_fderiv_undef, isClosed_le_of_isClosed_nonneg, pi_polarCoord_symm_target_ae_eq_univ, IsModuleTopology.continuous_bilinear_of_finite_right, ContinuousLinearMap.coe_prodMap, Complex.continuousAt_cpow_of_re_pos, NumberField.mixedEmbedding.measurableSet_negAt_plusPart, TopCat.prodIsoProd_inv_fst_apply, NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_symm_apply, ContinuousLinearMap.coprod_comp_inl, ContinuousLinearMap.norm_snd_le, SeparationQuotient.continuousOn_lift₂, DifferentiableOn.prodMk, continuousOn_cfc_nnreal_setProd, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, ContinuousAlgHom.coe_snd', mfderiv_fst, HasStrictFDerivAt.mem_implicitToPartialHomeomorph_source, Homeomorph.funSplitAt_apply, isClosedMap_fst_of_compactSpace, HasStrictFDerivAt.implicitToPartialHomeomorph_fst, HasStrictFDerivAt.mem_implicitToPartialHomeomorph_target, prod_nhdsSet_le_of_disjoint_cocompact, Prod.snd_exp, Trivialization.sourceHomeomorphBaseSetProd_apply, Trivialization.prod_apply', ContinuousLinearMap.prodₗ_apply, ContinuousLinearMap.coprodEquiv_symm_apply, Fin.continuous_append, ContinuousAffineMap.prod_toAffineMap, UniqueDiffWithinAt.prod, HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented_apply_ker, ProbabilityTheory.instIsGaussianProdProdOfSecondCountableTopologyEither, IsBoundedBilinearMap.differentiable, Inseparable.prod, MeasureTheory.AEEqFun.comp₂Measurable_eq_pair, instOrderClosedTopologyProd, SeparationQuotient.continuous_lift₂, Topology.isInducing_prod_const, UniformSpace.Completion.continuous_inner, LinearPMap.closure_inverse_graph, Path.Homotopic.comp_prod_eq_prod_comp, ContMDiffOn.clm_prodMap, continuousWithinAt_fst, ContinuousMap.snd_apply, instProperConstSMulProd, Bundle.Prod.contMDiffVectorBundle, instT3SpaceProd, EReal.nhds_coe_coe, ImplicitFunctionData.toPartialHomeomorph_apply, ContinuousLinearMap.prod_apply, ContinuousLinearMap.ker_coprod_of_disjoint_range, NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace, NumberField.mixedEmbedding.det_fderivPolarCoordRealSymm, UniqueMDiffWithinAt.prod, mdifferentiable_prod_module_iff, HasFDerivAt.prodMap, equivTangentBundleProd_symm_apply_proj, isOpenMap_prod_of_discrete_left, ContinuousLinearMap.norm_snd, isHomeomorphicTrivialFiberBundle_fst, Homeomorph.toEquiv_sigmaProdDistrib, LinearMap.IsContPerfPair.continuous_uncurry, Asymptotics.isBigOTVS_prodMk_left, ContMDiff.prodMk_space, ContMDiffWithinAt.prodMap, Bundle.Trivial.trivialization_symm_apply_proj, Homeomorph.prodCongr_symm, Continuous.prodMk_left, contMDiffAt_fst, mdifferentiableWithinAt_prod_iff, ContinuousMonoidHom.continuous_comp, Real.hasStrictFDerivAt_rpow_of_neg, Topology.IsQuotientMap.trivializationOfVAddDisjoint_target, intervalIntegral.integral_hasFDerivAt, ImplicitFunctionData.toOpenPartialHomeomorph_apply, ContinuousAdd.continuous_add, intervalIntegral.fderiv_integral, SeparationQuotient.map_prod_map_mk_nhds, ContinuousAt.prodMk, AddUnits.continuous_embedProduct, ContinuousMultilinearMap.sub_prod_sub, EReal.continuousAt_mul, ContinuousLinearEquiv.prodCongr_apply, HasStrictFDerivAt.inner, upperSemicontinuousOn_iff_isClosed_hypograph, InnerProductGeometry.continuousAt_angle, NumberField.mixedEmbedding.polarCoordReal_target, ContinuousMonoidHom.fst_toFun, Complex.polarCoord_target, FundamentalGroupoidFunctor.prodToProdTop_map, tangentMap_prod_right, Trivialization.frontier_preimage, ContinuousMultilinearMap.zero_prod_zero, Prod.instAlexandrovDiscrete, TopologicalSpace.Clopens.mem_prod, continuousAt_snd, FiberwiseLinear.trans_PartialHomeomorph_apply, instRegularSpaceProd, Homeomorph.piSplitAt_apply, Trivialization.codExtend'_source, ContinuousMultilinearMap.opNorm_prod, ContinuousWithinAt.prodMk, tangentMap_prod_left, ContinuousLinearMap.comp_fst_add_comp_snd, NumberField.mixedEmbedding.integral_comp_polarCoord_symm, SmoothBumpCovering.embeddingPiTangent_coe, ContinuousAlternatingMap.prodLIE_symm_apply, Homeomorph.sigmaProdDistrib_apply, ContinuousLinearMap.HasRightInverse.fst, OpenPartialHomeomorph.prod_trans, Homeomorph.prodComm_symm, FiberwiseLinear.source_trans_openPartialHomeomorph, ContinuousAlgHom.prod_apply, Prod.instBoundedGENhdsClass, ContinuousMap.continuous_curry, Trivialization.continuousOn_symm, continuousOn_cfcₙ_nnreal_setProd, contDiffGroupoid_prod, AddUnits.isClosedEmbedding_embedProduct, continuous_nndist, ContinuousAlternatingMap.opNNNorm_prod, ContinuousLinearMap.range_coprod, ModelWithCorners.interior_prod, continuous_prod_of_continuous_lipschitzWith', ContinuousLinearEquiv.prodAssoc_symm_apply, UniformSpace.hasBasis_nhds_prod, contMDiffOn_snd, continuous_max, Homeomorph.piFinTwo_symm_apply, ContinuousLinearEquiv.fst_equivOfRightInverse, mfderiv_prod_left, NumberField.mixedEmbedding.norm_negAt, continuousAt_fst, GenLoop.homotopyFrom_apply, MDifferentiableWithinAt.clm_prodMap, contMDiffOn_prod_module_iff, isLindelof_diagonal, fderivInnerCLM_apply, isClosed_le_prod, HasStrictFDerivAt.implicitToPartialHomeomorph_apply_ker, uniformity_hasBasis_open, Bundle.Trivial.homeomorphProd_apply, hasFDerivAt_fst, ContinuousLinearMap.coe_prod, MDifferentiableWithinAt.prodMap', OpenSubgroup.toSubgroup_prod, Trivialization.contMDiffOn, Filter.Tendsto.prodMap_nhds, CFC.rpow_eq_rpow_prod, GenLoop.fromLoop_coe, ContinuousMultilinearMap.hasStrictFDerivAt_uncurry, Units.isInducing_embedProduct, ContinuousSqrt.continuousOn_sqrt, MeasureTheory.charFunDual_eq_prod_iff', ContinuousAffineEquiv.prodAssoc_symm_apply, ContinuousLinearEquiv.equivOfRightInverse_symm_apply, differentiableOn_snd, RestrictedProduct.continuous_dom_prod_left, NumberField.mixedEmbedding.integral_comp_polarCoordReal_symm, ImplicitFunctionData.left_map_implicitFunction, Fin.consEquivL_symm_apply, hom_trivializationAt_target, IsPreconnected.prod, OpenAddSubgroup.coe_prod, contMDiff_fst, Bundle.Trivial.trivialization_source, boundary_product, integral_comp_pi_polarCoord_symm, MDifferentiableAt.prodMap, NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace, polarCoord_source, NumberField.mixedEmbedding.measurable_polarSpaceCoord_symm, Trivialization.mdifferentiable, ContinuousOn.continuousLinearMapCoprod, ContinuousAffineMap.coe_prod, VectorBundle.prod, LinearPMap.IsClosable.graph_closure_eq_closure_graph, ContinuousAffineMap.coe_prodMap, AddUnits.isEmbedding_embedProduct, nhdsSetWithin_prod_le, frontier_univ_prod_eq, ContinuousLinearMap.coprodEquivL_symm_apply, isBoundedLinearMap_prod_multilinear, ContMDiff.prodMap, ContinuousMultilinearMap.prod_apply, ContinuousOn.prod_map_equivL, differentiableWithinAt_fst, Filter.HasBasis.prod_nhds', ContinuousLinearEquiv.prodComm_toLinearEquiv, LinearMap.continuous_uncurry_of_isContPerfPair, ContinuousAlgHom.snd_comp_prod, ContinuousMonoidHom.prodMap_toFun, mem_contMDiffFiberwiseLinear_iff, Submodule.coe_prodEquivOfClosedCompl, isSeparatedMap_iff_isClosed_diagonal, AddUnits.isInducing_embedProduct, ContinuousLinearMap.fpowerSeriesBilinear_apply_one, Trivialization.prod_source, NumberField.mixedEmbedding.disjoint_negAt_plusPart, ContinuousMap.Homotopy.map_zero_left, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_source, HasStrictFDerivAt.eq_implicitFunction, CFC.nnrpow_map_prod, ContinuousLinearEquiv.piFinTwo_symm_apply, IsContDiffImplicitAt.implicitFunctionAux_fst, Trivialization.coordChangeL_apply', Bundle.Trivial.trivialization_symm_apply_snd, IsClopen.prod, ContinuousMultilinearMap.add_prod_add, FiberBundleCore.localTrivAsPartialEquiv_symm, Uniform.continuousAt_iff_prod, continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith, FiberBundleCore.localTrivAsPartialEquiv_trans, Complex.equivRealProdCLM_apply, ContinuousAlgHom.coe_snd, instT1SpaceProd, contMDiffAt_snd, EMetric.continuous_infEdist_hausdorffEdist, ContinuousAddMonoidHom.swap_toFun, IsOpen.prod, WithLp.prod_continuous_ofLp, ContinuousLinearMap.coe_deriv₂, Homeomorph.coe_punitProd, extChartAt_prod, Submodule.coe_prodEquivOfClosedCompl_symm, Continuous.prod_mapL, ENNReal.nhds_coe_coe, Filter.Tendsto.prodMk_nhds, FiberBundleCore.localTriv_symm_apply, isEmbedding_prodMkRight, TopologicalSpace.instSecondCountableTopologyProd, NonarchimedeanAddGroup.Prod.instNonarchimedeanAddGroup, ContinuousLinearMap.coprod_inl_inr, differentiableOn_fst, Dense.prod, hasFDerivWithinAt_snd, IsTopologicalAddGroup.continuous_addConj_prod, IsBoundedBilinearMap.differentiableWithinAt, NumberField.mixedEmbedding.fundamentalCone.logMap_normAtAllPlaces, closure_prod_eq, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, Continuous.mapPullback, IsModuleTopology.continuous_mul_of_finite, ContinuousLinearMap.continuousAt_uncurry_of_multilinear, LinearPMap.IsClosable.existsUnique, MeasureTheory.Measure.instIsOpenPosMeasureProdVolumeOfSFinite, NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlaces, TangentBundle.trivializationAt_target, ContinuousMap.prod_eval, ProbabilityTheory.IsGaussian.map_rotation_eq_self_of_forall_strongDual_eq_zero, GromovHausdorff.HD_below_aux1, norm_jacobiTheta₂_term_fderiv_le, MeasureTheory.AEEqFun.coeFn_pair, ContinuousLinearEquiv.piFinTwo_apply, Continuous.prodMk, TopCat.prodIsoProd_inv_snd_apply, Prod.continuousMul, hasFDerivAt_prodMk_right, UniqueDiffOn.prod, Manifold.LiftSourceTargetPropertyAt.prodMap, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_apply, FiberBundleCore.mem_trivChange_source, continuous_iff_continuous_dist, Prod.opensMeasurableSpace, NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply, Trivialization.restrictPreimage_target, ContMDiff.prodMk, NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm, WithLp.prodContinuousLinearEquiv_apply, Topology.IsOpenEmbedding.prodMap, Trivialization.coordChangeL_prod, Trivialization.source_eq
instTopologicalSpaceSum 📖	CompOp	133 math math: mfderiv_sumSwap, IsClosedMap.sumMap, ChartedSpace.sum_chartAt_inr, Sum.isGeneratedBy, AlgebraicGeometry.coprodSpec_apply, isOpen_sum_iff, continuous_sumMap, Topology.IsInducing.sumElim, Topology.IsEmbedding.inl, contMDiff_sum_map, continuous_sumElim, isClosedMap_inr, ModelWithCorners.interior_disjointUnion, hasMFDerivAt_sumSwap, Continuous.sumMap, continuous_inl, instSigmaCompactSpaceSum, extChartAt_inl_apply, IsOpenEmbedding.sumSwap, Homeomorph.sumSumSumComm_toEquiv, TopologicalSpace.IsTopologicalBasis.sum, IsClosedMap.sumElim, isEmbedding_sumElim, ContMDiff.inr, Diffeomorph.sumCongr_symm_symm, Sum.deltaGeneratedSpace, hasMFDerivAt_inr, AlgebraicGeometry.coprodMk_inl, mfderivWithin_sumInr, Sum.instAlexandrovDiscrete, Homeomorph.sumProdDistrib_symm_apply, Diffeomorph.sumAssoc_coe, continuous_inr, ModelWithCorners.boundaryPoint_inl, isClosed_range_inl, Diffeomorph.sumCongr_inl, isClopen_range_inl, ContMDiff.sumMap, isClosedMap_inl, hasMFDerivWithinAt_inr, mfderivWithin_sumInl, ContMDiff.inl, instTotallyDisconnectedSpaceSum, mfderiv_sumInl, ModelWithCorners.boundary_disjointUnion, ChartedSpace.sum_chartAt_inl, continuous_sum_swap, isInducing_sumElim, Diffeomorph.sumComm_coe, continuous_isRight, Topology.IsEmbedding.sumElim, TopologicalSpace.instSecondCountableTopologySum, Diffeomorph.sumComm_inr, nhds_inl, IsOpenEmbedding.sumElim, isClopen_range_inr, ContMDiff.swap, extChartAt_inr_apply, isOpen_range_inr, nhds_inr, Homeomorph.sumCongr_refl, Diffeomorph.sumCongr_coe, hasMFDerivAt_inl, Homeomorph.continuous_sumAssoc, Topology.IsOpenEmbedding.inr, IsManifold.disjointUnion, Sum.instSequentialSpace, IsClosedEmbedding.sumElim, Homeomorph.sumComm_symm, Topology.IsClosedEmbedding.inr, IsHomeomorph.sumMap, Homeomorph.continuous_sumAssoc_symm, AlgebraicGeometry.coprodSpec_coprodMk, Diffeomorph.sumCongr_inr, Homeomorph.sumProdDistrib_apply, TopologicalSpace.IsCompletelyMetrizableSpace.sum, instCompactSpaceSum, Diffeomorph.sumEmpty_apply_inl, TopologicalSpace.instSeparableSpaceSum, isClosedMap_sumElim, Topology.IsInducing.sumElim_of_separatedNhds, Topology.IsClosedEmbedding.inl, ModelWithCorners.boundaryPoint_inr, ModelWithCorners.boundaryless_disjointUnion, mfderiv_sumInr, ContMDiff.sumElim, GromovHausdorff.HD_below_aux2, isOpenMap_sum, isOpenMap_inl, isClosed_range_inr, writtenInExtChartAt_sumSwap_eventuallyEq_id, Topology.IsOpenEmbedding.inl, Homeomorph.coe_emptySum, Homeomorph.sumSumSumComm_symm, instT2SpaceSum, Topology.IsEmbedding.sumElim_of_separatedNhds, Homeomorph.sumAssoc_toEquiv, isOpenMap_sumElim, Homeomorph.sumCongr_symm, isClosedMap_sum, Sum.isPreconnected_iff, isClosed_sum_iff, Sum.isConnected_iff, Diffeomorph.sumEmpty_toEquiv, IsOpenMap.sumMap, continuous_isLeft, Sum.locPathConnectedSpace, instLindelofSpaceSum, TopologicalSpace.separableSpace_sum_iff, continuous_sum_dom, isOpenMap_inr, Diffeomorph.sumComm_inl, instUCompactlyGeneratedSpaceSum, writtenInExtChartAt_sumInr_eventuallyEq_id, IsInducing.sumSwap, Homeomorph.coe_sumComm, Continuous.sumElim, isOpen_range_inl, Homeomorph.sumCongr_trans, hasMFDerivWithinAt_inl, TopologicalSpace.IsCompletelyPseudoMetrizableSpace.sum, Diffeomorph.sumComm_symm, sum_chartAt_inl_apply, AlgebraicGeometry.coprodMk_inr, writtenInExtChartAt_sumInl_eventuallyEq_id, IsOpenMap.sumElim, ModelWithCorners.interiorPoint_inl, Homeomorph.sumEmpty_apply, ModelWithCorners.interiorPoint_inr, GromovHausdorff.HD_below_aux1, Sum.discreteTopology, sum_chartAt_inr_apply, Topology.IsEmbedding.inr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_prod_eq 📖	mathematical	—	closure instTopologicalSpaceProd SProd.sprod Set Set.instSProd	—	Set.ext nhdsWithin_prod_eq
continuousAt_fst 📖	mathematical	—	ContinuousAt instTopologicalSpaceProd	—	Continuous.continuousAt continuous_fst
continuousAt_snd 📖	mathematical	—	ContinuousAt instTopologicalSpaceProd	—	Continuous.continuousAt continuous_snd
continuous_curry 📖	—	Continuous instTopologicalSpaceProd	—	—	Continuous.uncurry_left
continuous_fst 📖	mathematical	—	Continuous instTopologicalSpaceProd	—	continuous_prodMk continuous_id
continuous_inf_dom_left₂ 📖	mathematical	Continuous instTopologicalSpaceProd	TopologicalSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	continuous_inf_dom_left continuous_id Continuous.prodMap Continuous.comp
continuous_inf_dom_right₂ 📖	mathematical	Continuous instTopologicalSpaceProd	TopologicalSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	continuous_inf_dom_right continuous_id Continuous.prodMap Continuous.comp
continuous_inl 📖	mathematical	—	Continuous instTopologicalSpaceSum	—	—
continuous_inr 📖	mathematical	—	Continuous instTopologicalSpaceSum	—	—
continuous_isLeft 📖	mathematical	—	Continuous instTopologicalSpaceSum instTopologicalSpaceBool	—	continuous_sum_dom continuous_const
continuous_isRight 📖	mathematical	—	Continuous instTopologicalSpaceSum instTopologicalSpaceBool	—	continuous_sum_dom continuous_const
continuous_prodMk 📖	mathematical	—	Continuous instTopologicalSpaceProd	—	continuous_inf_rng Iff.and continuous_induced_rng
continuous_sInf_dom₂ 📖	mathematical	TopologicalSpace Set Set.instMembership Continuous instTopologicalSpaceProd	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	continuous_sInf_dom continuous_id Continuous.prodMap Continuous.comp
continuous_snd 📖	mathematical	—	Continuous instTopologicalSpaceProd	—	continuous_prodMk continuous_id
continuous_sumElim 📖	mathematical	—	Continuous instTopologicalSpaceSum	—	continuous_sum_dom
continuous_sumMap 📖	mathematical	—	Continuous instTopologicalSpaceSum	—	continuous_sumElim Iff.and Topology.IsEmbedding.continuous_iff Topology.IsEmbedding.inl Topology.IsEmbedding.inr
continuous_sum_dom 📖	mathematical	—	Continuous instTopologicalSpaceSum	—	continuous_sup_dom Iff.and continuous_coinduced_dom
continuous_sum_swap 📖	mathematical	—	Continuous instTopologicalSpaceSum	—	Continuous.sumElim continuous_inr continuous_inl
continuous_swap 📖	mathematical	—	Continuous instTopologicalSpaceProd	—	Continuous.prodMk continuous_snd continuous_fst
exists_nhds_square 📖	mathematical	Set Filter Filter.instMembership nhds instTopologicalSpaceProd	IsOpen Set.instMembership Set.instHasSubset SProd.sprod Set.instSProd	—	nhds_prod_eq Filter.HasBasis.mem_iff Filter.HasBasis.prod_self nhds_basis_opens
frontier_prod_eq 📖	mathematical	—	frontier instTopologicalSpaceProd SProd.sprod Set Set.instSProd Set.instUnion closure	—	closure_prod_eq interior_prod_eq Set.prod_diff_prod
frontier_prod_univ_eq 📖	mathematical	—	frontier instTopologicalSpaceProd SProd.sprod Set Set.instSProd Set.univ	—	frontier_prod_eq frontier_univ Set.prod_empty IsClosed.closure_eq Set.empty_union
frontier_univ_prod_eq 📖	mathematical	—	frontier instTopologicalSpaceProd SProd.sprod Set Set.instSProd Set.univ	—	frontier_prod_eq IsClosed.closure_eq frontier_univ Set.empty_prod Set.union_empty
instDiscreteTopologyProd 📖	mathematical	—	DiscreteTopology instTopologicalSpaceProd	—	discreteTopology_iff_nhds nhds_prod_eq nhds_discrete Filter.prod_pure_pure
interior_prod_eq 📖	mathematical	—	interior instTopologicalSpaceProd SProd.sprod Set Set.instSProd	—	Set.ext
isClosedMap_inl 📖	mathematical	—	IsClosedMap instTopologicalSpaceSum	—	Set.preimage_image_eq Sum.inl_injective Set.preimage_inr_image_inl
isClosedMap_inr 📖	mathematical	—	IsClosedMap instTopologicalSpaceSum	—	Set.preimage_inl_image_inr Set.preimage_image_eq Sum.inr_injective
isClosedMap_sum 📖	mathematical	—	IsClosedMap instTopologicalSpaceSum	—	IsClosedMap.comp Topology.IsClosedEmbedding.isClosedMap Topology.IsClosedEmbedding.inl Topology.IsClosedEmbedding.inr Set.ext IsClosed.union isClosed_sum_iff
isClosedMap_sumElim 📖	mathematical	—	IsClosedMap instTopologicalSpaceSum	—	—
isClosedMap_swap 📖	mathematical	—	IsClosedMap instTopologicalSpaceProd	—	Set.image_swap_eq_preimage_swap IsClosed.preimage continuous_swap
isClosed_range_inl 📖	mathematical	—	IsClosed instTopologicalSpaceSum Set.range	—	isOpen_compl_iff Set.compl_range_inl isOpen_range_inr
isClosed_range_inr 📖	mathematical	—	IsClosed instTopologicalSpaceSum Set.range	—	isOpen_compl_iff Set.compl_range_inr isOpen_range_inl
isClosed_sum_iff 📖	mathematical	—	IsClosed instTopologicalSpaceSum Set.preimage	—	—
isEmbedding_graph 📖	mathematical	Continuous	Topology.IsEmbedding instTopologicalSpaceProd	—	Topology.IsEmbedding.of_comp Continuous.prodMk continuous_id continuous_fst Topology.IsEmbedding.id
isEmbedding_prodMkLeft 📖	mathematical	—	Topology.IsEmbedding instTopologicalSpaceProd	—	Topology.IsEmbedding.of_comp Continuous.prodMk_left continuous_fst Topology.IsEmbedding.id
isEmbedding_prodMkRight 📖	mathematical	—	Topology.IsEmbedding instTopologicalSpaceProd	—	Topology.IsEmbedding.of_comp Continuous.prodMk_right continuous_snd Topology.IsEmbedding.id
isEmbedding_sumElim 📖	mathematical	—	Topology.IsEmbedding instTopologicalSpaceSum Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice closure Set.range	—	Disjoint.ne_of_mem Set.mem_range_self subset_closure
isInducing_prodMkLeft 📖	mathematical	—	Topology.IsInducing instTopologicalSpaceProd	—	Topology.IsInducing.of_comp Continuous.prodMk_left continuous_fst Topology.IsInducing.id
isInducing_prodMkRight 📖	mathematical	—	Topology.IsInducing instTopologicalSpaceProd	—	Topology.IsInducing.of_comp Continuous.prodMk_right continuous_snd Topology.IsInducing.id
isInducing_sumElim 📖	mathematical	—	Topology.IsInducing instTopologicalSpaceSum Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice closure Set.range	—	Topology.IsInducing.sumElim_left Topology.IsInducing.sumElim_right Topology.IsInducing.disjoint_of_sumElim_aux Disjoint.symm Topology.IsInducing.comp IsInducing.sumSwap Sum.elim_swap Topology.IsInducing.sumElim
isOpenMap_fst 📖	mathematical	—	IsOpenMap instTopologicalSpaceProd	—	isOpenMap_iff_nhds_le Eq.ge map_fst_nhds
isOpenMap_inl 📖	mathematical	—	IsOpenMap instTopologicalSpaceSum	—	Set.preimage_image_eq Sum.inl_injective Set.preimage_inr_image_inl
isOpenMap_inr 📖	mathematical	—	IsOpenMap instTopologicalSpaceSum	—	Set.preimage_inl_image_inr Set.preimage_image_eq Sum.inr_injective
isOpenMap_snd 📖	mathematical	—	IsOpenMap instTopologicalSpaceProd	—	isOpenMap_iff_nhds_le Eq.ge map_snd_nhds
isOpenMap_sum 📖	mathematical	—	IsOpenMap instTopologicalSpaceSum	—	nhds_inl Filter.map_map nhds_inr
isOpenMap_sumElim 📖	mathematical	—	IsOpenMap instTopologicalSpaceSum	—	—
isOpen_prod_iff 📖	mathematical	—	IsOpen instTopologicalSpaceProd Set Set.instMembership Set.instHasSubset SProd.sprod Set.instSProd	—	isOpen_iff_mem_nhds
isOpen_prod_iff' 📖	mathematical	—	IsOpen instTopologicalSpaceProd SProd.sprod Set Set.instSProd Set.instEmptyCollection	—	Set.eq_empty_or_nonempty Set.prod_eq_empty_iff Set.prod_nonempty_iff Set.fst_image_prod isOpenMap_fst Set.snd_image_prod isOpenMap_snd IsOpen.prod Set.Nonempty.ne_empty
isOpen_range_inl 📖	mathematical	—	IsOpen instTopologicalSpaceSum Set.range	—	Topology.IsOpenEmbedding.isOpen_range Topology.IsOpenEmbedding.inl
isOpen_range_inr 📖	mathematical	—	IsOpen instTopologicalSpaceSum Set.range	—	Topology.IsOpenEmbedding.isOpen_range Topology.IsOpenEmbedding.inr
isOpen_setOf_disjoint_nhds_nhds 📖	mathematical	—	IsOpen instTopologicalSpaceProd setOf Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhds	—	Filter.HasBasis.disjoint_iff nhds_basis_opens mem_nhds_prod_iff' Filter.disjoint_of_disjoint_of_mem IsOpen.mem_nhds
isOpen_sum_iff 📖	mathematical	—	IsOpen instTopologicalSpaceSum Set.preimage	—	—
isQuotientMap_fst 📖	mathematical	—	Topology.IsQuotientMap instTopologicalSpaceProd	—	IsOpenMap.isQuotientMap isOpenMap_fst continuous_fst Prod.fst_surjective
isQuotientMap_snd 📖	mathematical	—	Topology.IsQuotientMap instTopologicalSpaceProd	—	IsOpenMap.isQuotientMap isOpenMap_snd continuous_snd Prod.snd_surjective
map_fst_nhds 📖	mathematical	—	Filter.map nhds instTopologicalSpaceProd	—	le_antisymm continuousAt_fst Eq.trans_le map_fst_nhdsWithin Filter.map_mono inf_le_left
map_fst_nhdsWithin 📖	mathematical	—	Filter.map nhdsWithin instTopologicalSpaceProd Set.preimage Set Set.instSingletonSet nhds	—	le_antisymm Filter.Tendsto.mono_left continuousAt_fst inf_le_left mem_nhds_prod_iff Filter.mem_inf_principal nhdsWithin.eq_1 Filter.mem_map Filter.mem_of_superset mem_of_mem_nhds
map_mem_closure₂ 📖	—	Continuous instTopologicalSpaceProd Set Set.instMembership closure	—	—	closure_prod_eq Set.mk_mem_prod Set.forall_prod_set Set.MapsTo.closure
map_snd_nhds 📖	mathematical	—	Filter.map nhds instTopologicalSpaceProd	—	le_antisymm continuousAt_snd Eq.trans_le map_snd_nhdsWithin Filter.map_mono inf_le_left
map_snd_nhdsWithin 📖	mathematical	—	Filter.map nhdsWithin instTopologicalSpaceProd Set.preimage Set Set.instSingletonSet nhds	—	le_antisymm Filter.Tendsto.mono_left continuousAt_snd inf_le_left mem_nhds_prod_iff Filter.mem_inf_principal nhdsWithin.eq_1 Filter.mem_map Filter.mem_of_superset mem_of_mem_nhds
mem_nhdsWithin_prod_iff 📖	mathematical	—	Set Filter Filter.instMembership nhdsWithin instTopologicalSpaceProd SProd.sprod Set.instSProd Set.instHasSubset	—	nhdsWithin_prod_eq Filter.mem_prod_iff
mem_nhds_prod_iff 📖	mathematical	—	Set Filter Filter.instMembership nhds instTopologicalSpaceProd Set.instHasSubset SProd.sprod Set.instSProd	—	nhds_prod_eq Filter.mem_prod_iff
mem_nhds_prod_iff' 📖	mathematical	—	Set Filter Filter.instMembership nhds instTopologicalSpaceProd IsOpen Set.instMembership Set.instHasSubset SProd.sprod Set.instSProd	—	Filter.HasBasis.mem_iff Filter.HasBasis.prod_nhds nhds_basis_opens
nhdsWithin_prod_eq 📖	mathematical	—	nhdsWithin instTopologicalSpaceProd SProd.sprod Set Set.instSProd Filter Filter.instSProd	—	nhds_prod_eq Filter.prod_principal_principal
nhds_inl 📖	mathematical	—	nhds instTopologicalSpaceSum Filter.map	—	Topology.IsOpenEmbedding.map_nhds_eq Topology.IsOpenEmbedding.inl
nhds_inr 📖	mathematical	—	nhds instTopologicalSpaceSum Filter.map	—	Topology.IsOpenEmbedding.map_nhds_eq Topology.IsOpenEmbedding.inr
nhds_prod_eq 📖	mathematical	—	nhds instTopologicalSpaceProd SProd.sprod Filter Filter.instSProd	—	Filter.prod_eq_inf instTopologicalSpaceProd.eq_1 nhds_inf nhds_induced
nhds_swap 📖	mathematical	—	nhds instTopologicalSpaceProd Filter.map	—	nhds_prod_eq Filter.prod_comm
prod_eq_generateFrom 📖	mathematical	—	instTopologicalSpaceProd TopologicalSpace.generateFrom setOf Set IsOpen SProd.sprod Set.instSProd	—	le_antisymm le_generateFrom IsOpen.prod le_inf Set.forall_mem_image Set.inter_univ Set.univ_inter
prod_generateFrom_generateFrom_eq 📖	mathematical	Set.sUnion Set.univ	instTopologicalSpaceProd TopologicalSpace.generateFrom Set.image2 Set SProd.sprod Set.instSProd	—	le_antisymm le_generateFrom IsOpen.prod le_inf coinduced_le_iff_le_induced Set.prod_univ isOpen_iUnion Set.univ_prod
prod_induced_induced 📖	mathematical	—	instTopologicalSpaceProd TopologicalSpace.induced	—	induced_inf induced_compose
prod_mem_nhds 📖	mathematical	Set Filter Filter.instMembership nhds	instTopologicalSpaceProd SProd.sprod Set.instSProd	—	prod_mem_nhds_iff
prod_mem_nhds_iff 📖	mathematical	—	Set Filter Filter.instMembership nhds instTopologicalSpaceProd SProd.sprod Set.instSProd	—	nhds_prod_eq Filter.prod_mem_prod_iff nhds_neBot

---

← Back to Index