ReImTopology

📁 Source: Mathlib/Analysis/Complex/ReImTopology.lean

Statistics

Metric	Count
Definitions	0
Theorems reProdIm, closure_preimage_im, closure_preimage_re, closure_reProdIm, closure_setOf_im_lt, closure_setOf_lt_im, closure_setOf_lt_re, closure_setOf_re_lt, frontier_preimage_im, frontier_preimage_re, frontier_reProdIm, frontier_setOf_im_le, frontier_setOf_im_lt, frontier_setOf_le_im, frontier_setOf_le_re, frontier_setOf_le_re_and_im_le, frontier_setOf_le_re_and_le_im, frontier_setOf_lt_im, frontier_setOf_lt_re, frontier_setOf_re_le, frontier_setOf_re_lt, interior_preimage_im, interior_preimage_re, interior_reProdIm, interior_setOf_im_le, interior_setOf_le_im, interior_setOf_le_re, interior_setOf_re_le, isHomeomorphicTrivialFiberBundle_im, isHomeomorphicTrivialFiberBundle_re, isOpenMap_im, isOpenMap_re, isQuotientMap_im, isQuotientMap_re, reProdIm, reProdIm, im, re, im, re	40
Total	40

Bornology.IsBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reProdIm 📖	mathematical	Bornology.IsBounded Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace	Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.reProdIm	—	AntilipschitzWith.isBounded_preimage Nat.instAtLeastTwoHAddOfNat Complex.antilipschitz_equivRealProd prod

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_preimage_im 📖	mathematical	—	closure Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Set.preimage Real im Real.pseudoMetricSpace	—	IsOpenMap.preimage_closure_eq_closure_preimage isOpenMap_im continuous_im
closure_preimage_re 📖	mathematical	—	closure Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Set.preimage Real re Real.pseudoMetricSpace	—	IsOpenMap.preimage_closure_eq_closure_preimage isOpenMap_re continuous_re
closure_reProdIm 📖	mathematical	—	closure Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField reProdIm Real Real.pseudoMetricSpace	—	RingHomInvPair.ids Set.preimage_eq_preimage Homeomorph.surjective Homeomorph.preimage_closure closure_prod_eq
closure_setOf_im_lt 📖	mathematical	—	closure Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLT im Real.instLE	—	closure_Iio instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial closure_preimage_im
closure_setOf_lt_im 📖	mathematical	—	closure Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLT im Real.instLE	—	closure_Ioi instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial closure_preimage_im
closure_setOf_lt_re 📖	mathematical	—	closure Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLT re Real.instLE	—	closure_Ioi instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial closure_preimage_re
closure_setOf_re_lt 📖	mathematical	—	closure Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLT re Real.instLE	—	closure_Iio instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial closure_preimage_re
frontier_preimage_im 📖	mathematical	—	frontier Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Set.preimage Real im Real.pseudoMetricSpace	—	IsOpenMap.preimage_frontier_eq_frontier_preimage isOpenMap_im continuous_im
frontier_preimage_re 📖	mathematical	—	frontier Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Set.preimage Real re Real.pseudoMetricSpace	—	IsOpenMap.preimage_frontier_eq_frontier_preimage isOpenMap_re continuous_re
frontier_reProdIm 📖	mathematical	—	frontier Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField reProdIm Set Set.instUnion closure Real Real.pseudoMetricSpace	—	RingHomInvPair.ids Set.preimage_eq_preimage Homeomorph.surjective Homeomorph.preimage_frontier frontier_prod_eq
frontier_setOf_im_le 📖	mathematical	—	frontier Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLE im	—	frontier_Iic instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial frontier_preimage_im
frontier_setOf_im_lt 📖	mathematical	—	frontier Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLT im	—	frontier_Iio instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial frontier_preimage_im
frontier_setOf_le_im 📖	mathematical	—	frontier Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLE im	—	frontier_Ici instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial frontier_preimage_im
frontier_setOf_le_re 📖	mathematical	—	frontier Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLE re	—	frontier_Ici instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial frontier_preimage_re
frontier_setOf_le_re_and_im_le 📖	mathematical	—	frontier Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLE re im	—	closure_Ici instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal frontier_Iic LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial frontier_Ici instNoMinOrderOfNontrivial closure_Iic instClosedIicTopology frontier_reProdIm
frontier_setOf_le_re_and_le_im 📖	mathematical	—	frontier Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLE re im	—	closure_Ici instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal frontier_Ici LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial frontier_reProdIm
frontier_setOf_lt_im 📖	mathematical	—	frontier Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLT im	—	frontier_Ioi instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial frontier_preimage_im
frontier_setOf_lt_re 📖	mathematical	—	frontier Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLT re	—	frontier_Ioi instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial frontier_preimage_re
frontier_setOf_re_le 📖	mathematical	—	frontier Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLE re	—	frontier_Iic instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial frontier_preimage_re
frontier_setOf_re_lt 📖	mathematical	—	frontier Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLT re	—	frontier_Iio instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial frontier_preimage_re
interior_preimage_im 📖	mathematical	—	interior Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Set.preimage Real im Real.pseudoMetricSpace	—	IsOpenMap.preimage_interior_eq_interior_preimage isOpenMap_im continuous_im
interior_preimage_re 📖	mathematical	—	interior Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Set.preimage Real re Real.pseudoMetricSpace	—	IsOpenMap.preimage_interior_eq_interior_preimage isOpenMap_re continuous_re
interior_reProdIm 📖	mathematical	—	interior Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField reProdIm Real Real.pseudoMetricSpace	—	reProdIm.eq_1 interior_inter interior_preimage_re interior_preimage_im
interior_setOf_im_le 📖	mathematical	—	interior Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLE im Real.instLT	—	interior_Iic instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial interior_preimage_im
interior_setOf_le_im 📖	mathematical	—	interior Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLE im Real.instLT	—	interior_Ici instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial interior_preimage_im
interior_setOf_le_re 📖	mathematical	—	interior Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLE re Real.instLT	—	interior_Ici instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial interior_preimage_re
interior_setOf_re_le 📖	mathematical	—	interior Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField setOf Real Real.instLE re Real.instLT	—	interior_Iic instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial interior_preimage_re
isHomeomorphicTrivialFiberBundle_im 📖	mathematical	—	IsHomeomorphicTrivialFiberBundle Real Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField im	—	RingHomInvPair.ids
isHomeomorphicTrivialFiberBundle_re 📖	mathematical	—	IsHomeomorphicTrivialFiberBundle Real Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField re	—	RingHomInvPair.ids
isOpenMap_im 📖	mathematical	—	IsOpenMap Complex Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Real.pseudoMetricSpace im	—	IsHomeomorphicTrivialFiberBundle.isOpenMap_proj isHomeomorphicTrivialFiberBundle_im
isOpenMap_re 📖	mathematical	—	IsOpenMap Complex Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Real.pseudoMetricSpace re	—	IsHomeomorphicTrivialFiberBundle.isOpenMap_proj isHomeomorphicTrivialFiberBundle_re
isQuotientMap_im 📖	mathematical	—	Topology.IsQuotientMap Complex Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Real.pseudoMetricSpace im	—	IsHomeomorphicTrivialFiberBundle.isQuotientMap_proj isHomeomorphicTrivialFiberBundle_im
isQuotientMap_re 📖	mathematical	—	Topology.IsQuotientMap Complex Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Real.pseudoMetricSpace re	—	IsHomeomorphicTrivialFiberBundle.isQuotientMap_proj isHomeomorphicTrivialFiberBundle_re

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reProdIm 📖	mathematical	—	IsClosed Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.reProdIm	—	inter preimage Complex.continuous_re Complex.continuous_im

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reProdIm 📖	mathematical	IsOpen Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.reProdIm	—	inter preimage Complex.continuous_re Complex.continuous_im

TendstoUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
im 📖	mathematical	TendstoUniformly Complex PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	Real Real.pseudoMetricSpace Complex.im	—	UniformContinuous.comp_tendstoUniformly Complex.uniformContinuous_im
re 📖	mathematical	TendstoUniformly Complex PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	Real Real.pseudoMetricSpace Complex.re	—	UniformContinuous.comp_tendstoUniformly Complex.uniformContinuous_re

TendstoUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
im 📖	mathematical	TendstoUniformlyOn Complex PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	Real Real.pseudoMetricSpace Complex.im	—	UniformContinuous.comp_tendstoUniformlyOn Complex.uniformContinuous_im
re 📖	mathematical	TendstoUniformlyOn Complex PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	Real Real.pseudoMetricSpace Complex.re	—	UniformContinuous.comp_tendstoUniformlyOn Complex.uniformContinuous_re

---

← Back to Index