Weierstrass

📁 Source: Mathlib/Topology/ContinuousMap/Weierstrass.lean

Statistics

Metric	Count
Definitions	0
Theorems continuousMap_mem_polynomialFunctions_closure, exists_polynomial_near_continuousMap, exists_polynomial_near_of_continuousOn, polynomialFunctions_closure_eq_top, polynomialFunctions_closure_eq_top'	5
Total	5

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousMap_mem_polynomialFunctions_closure 📖	mathematical	—	ContinuousMap Set.Elem Real Set.Icc Real.instPreorder instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Subalgebra Real.instCommSemiring ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal ContinuousMap.algebra Algebra.id SetLike.instMembership Subalgebra.instSetLike Subalgebra.topologicalClosure ContinuousMap.compactOpen ContinuousMap.instIsTopologicalSemiringOfLocallyCompactSpace locallyCompact_of_proper Subtype.pseudoMetricSpace proper_of_compact compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace Real.instConditionallyCompleteLinearOrder instOrderTopologyReal NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring polynomialFunctions	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMap.instIsTopologicalSemiringOfLocallyCompactSpace locallyCompact_of_proper proper_of_compact compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal polynomialFunctions_closure_eq_top
exists_polynomial_near_continuousMap 📖	mathematical	Real Real.instLT Real.instZero	Norm.norm ContinuousMap Set.Elem Set.Icc Real.instPreorder instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instNorm compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace Real.instConditionallyCompleteLinearOrder instOrderTopologyReal NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousMap.instSubOfContinuousSub Real.instSub IsTopologicalAddGroup.to_continuousSub Real.instAddGroup instIsTopologicalAddGroupReal Polynomial.toContinuousMapOn Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal mem_closure_iff_frequently continuousMap_mem_polynomialFunctions_closure compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Filter.HasBasis.frequently_iff Metric.nhds_basis_ball dist_eq_norm Metric.mem_ball
exists_polynomial_near_of_continuousOn 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc Real.instPreorder Real.instLT Real.instZero	abs Real.lattice Real.instAddGroup Real.instSub Polynomial.eval Real.semiring	—	continuousOn_iff_continuous_restrict compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal exists_polynomial_near_continuousMap ContinuousMap.norm_lt_iff
polynomialFunctions_closure_eq_top 📖	mathematical	—	Subalgebra.topologicalClosure Real Real.instCommSemiring ContinuousMap Set.Elem Set.Icc Real.instPreorder instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal ContinuousMap.compactOpen ContinuousMap.algebra Algebra.id ContinuousMap.instIsTopologicalSemiringOfLocallyCompactSpace locallyCompact_of_proper Subtype.pseudoMetricSpace proper_of_compact compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace Real.instConditionallyCompleteLinearOrder instOrderTopologyReal NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring polynomialFunctions Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMap.instIsTopologicalSemiringOfLocallyCompactSpace locallyCompact_of_proper proper_of_compact compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal lt_or_ge Homeomorph.instContinuousMapClass Real.instIsStrictOrderedRing polynomialFunctions_closure_eq_top' ContinuousMap.instIsTopologicalRingOfLocallyCompactSpace polynomialFunctions.comap_compRightAlgHom_iccHomeoI Subalgebra.topologicalClosure_comap_homeomorph Algebra.comap_top ContinuousMap.subsingleton_subalgebra Set.Subsingleton.coe_sort Set.subsingleton_Icc_of_ge
polynomialFunctions_closure_eq_top' 📖	mathematical	—	Subalgebra.topologicalClosure Real Real.instCommSemiring ContinuousMap Set.Elem unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal ContinuousMap.compactOpen ContinuousMap.algebra Algebra.id ContinuousMap.instIsTopologicalSemiringOfLocallyCompactSpace locallyCompact_of_proper Subtype.pseudoMetricSpace proper_of_compact compactSpace_Icc Real.instPreorder ConditionallyCompleteLinearOrder.toCompactIccSpace Real.instConditionallyCompleteLinearOrder instOrderTopologyReal Real.instZero Real.instOne NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring polynomialFunctions Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_unique IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMap.instIsTopologicalSemiringOfLocallyCompactSpace locallyCompact_of_proper proper_of_compact compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal mem_closure_of_tendsto instIsTopologicalAddGroupReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat bernsteinApproximation_uniform NormedSpace.toLocallyConvexSpace Filter.Eventually.of_forall Subalgebra.sum_mem SetLike.mem_coe polynomialFunctions_coe ContinuousMap.ext Polynomial.eval_mul Polynomial.eval_C

---

← Back to Index