Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Sequentially Compact Subset of a Metric Space
definitiondef:sequentially-compact-subset-metric-2026aAnalysisTopologyLet be a metric space, and let . We say that is sequentially compact in if for every sequence in with for every , there exist a point and a strictly increasing sequence…A Cluster Point of a Sequence in a Metric Space is the Limit of a Subsequence
theoremthm:cluster-point-subsequence-metric-2026aAnalysisTopologyLet be a metric space, let be a sequence in , and let be a cluster point of in . Let be a sequence in the real numbers with for every …Every Sequence in a Compact Subset of a Metric Space Has a Cluster Point There
theoremthm:compact-sequence-cluster-point-metric-2026bAnalysisTopologyLet be a metric space, and let be the collection of subsets of that are open in , which is a topology on by Metric Open Sets Form a Topology. Let be compact in , and let be a…Cluster Point of a Sequence in a Metric Space
definitiondef:cluster-point-sequence-metric-2026aAnalysisTopologyLet be a metric space, let be a sequence in indexed by the natural numbers with the order , and let . We say that is a cluster point of in if for every real number and every…The Squared-Distance Penalization Limit on a Compact Set
corollarycor:penalization-limit-squared-distance-2026bAnalysisTopologyLet be a metric space, equipped with the collection of its subsets that are open in , a topology by Metric Open Sets Form a Topology, and let be nonempty and compact in . Let be the set of real numbers with the addition, multiplicatio…Limits of Penalized Maxima on a Compact Set
theoremthm:penalization-limit-compact-2026bAnalysisTopologyLet be a metric space, equipped with the collection of its subsets that are open in , a topology by Metric Open Sets Form a Topology, and let be nonempty and compact in . Let be the set of real numbers with the addition, multiplicatio…The Square of a Nonnegative Continuous Real-Valued Function is Continuous
lemmalem:square-nonnegative-continuous-2026aAnalysisTopologyLet be a metric space, let , and let be the set of real numbers with the addition, multiplication and order of its ordered field structure, regarded as a metric space through the metric of…Semicontinuity via Sublevel and Superlevel Sets
lemmalem:semicontinuity-sublevel-superlevel-2026aAnalysisTopologyLet be a metric space, let , and let be the restriction of to , a metric on by claim 1 of The Restriction of a Metric to a Subset Induces the Subspace Topology. Equip with the collection of its subsets that are open in , which i…Semicontinuity and Continuity Under Composition with a Continuous Map
lemmalem:semicontinuity-composition-continuous-2026aAnalysisTopologyLet and be metric spaces, let and , and let be the set of real numbers with the addition and the order of its ordered field structure, regarded as a metric space through the metric of…Continuity of the Projections and of the Distance Function on a Product Metric Space
lemmalem:projection-distance-continuous-product-2026aAnalysisTopologyLet be the set of real numbers with the addition, multiplication and order of its ordered field structure, regarded as a metric space through the metric of The Absolute Value Metric on the Real Line. Then the following hold. 1. (Projections) L…A Product of Compact Subsets is Compact in the Product Metric
corollarycor:product-compact-subsets-metric-2026bAnalysisTopologyLet and be metric spaces, each equipped with the collection of its subsets that are open in the respective metric space, a topology by Metric Open Sets Form a Topology. Let be compact in and let be compact in . Equip…The Product Metric Induces the Product Topology
theoremthm:product-metric-induces-product-topology-2026aAnalysisTopologyLet and be metric spaces. Let be the collection of all subsets open in and let be the collection of all subsets open in ; both are topologies by Metric Open Sets Form a Topology. Let be the…The Restriction of a Metric to a Subset Induces the Subspace Topology
lemmalem:restricted-metric-subspace-topology-2026aAnalysisTopologyLet be a metric space, let , and let be the set of real numbers. Let be the restriction of , that is, the function with for all . Equip with the collection of all su…- Let and be metric spaces and let be the product metric on . Let be the set of real numbers with the addition and the order of its ordered field structure, and for write to mean that…
Product Metric on the Cartesian Product of Two Metric Spaces
definitiondef:product-metric-2026aAnalysisTopologyLet and be metric spaces, and let be the Cartesian product of the sets and . Let be the set of real numbers with the order of its ordered field structure, which is in particular a total order. The product metric on…Euclidean Continuity Agrees with Metric Continuity for Real-Valued Functions
lemmalem:euclidean-metric-continuity-agree-2026aAnalysisTopologyMultivariable CalculusLet be a natural number, let be a subset of Euclidean space , let be the set of real numbers with the operations and the order of its ordered field structure, where for we write to mean that…The Euclidean Distance on the Real Line is the Absolute Value Metric
lemmalem:euclidean-distance-real-line-2026bAnalysisTopologyLet be the set of real numbers, let be the absolute value on , let be the metric of The Absolute Value Metric on the Real Line, and let be the Euclidean distance on in the case , with…Local Minimum of a Function Relative to a Subset of a Metric Space
definitiondef:local-minimum-metric-2026aAnalysisTopologyLet be a metric space, let , let be the set of real numbers with the order of its ordered field structure, where means that and , let , and let . We say that has a…Local Maximum of a Function Relative to a Subset of a Metric Space
definitiondef:local-maximum-metric-2026aAnalysisTopologyLet be a metric space, let , let be the set of real numbers with the order of its ordered field structure, where means that and , let , and let . We say that has a…Semicontinuous Functions Attain Their Extrema on a Compact Set
theoremthm:semicontinuous-attains-extrema-compact-2026bAnalysisTopologyLet be a metric space, equipped with the collection of all subsets that are open in , which is a topology by Metric Open Sets Form a Topology. Let be nonempty and compact in . Let be the set of real numbers with the order of its…