Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- Let be a nonempty set, let denote the natural numbers, and let be a binary relation on , that is, a subset of the Cartesian product . Assume that for every there exists with . Let . Then there exists a…
A Compact Subset of a Metric Space is Totally Bounded
theoremthm:compact-implies-totally-bounded-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 . Then is totally bounded in .Totally Bounded Subset of a Metric Space
definitiondef:totally-bounded-subset-metric-2026aAnalysisTopologyLet be a metric space, and let . We say that is totally bounded in if for every real number there exists a finite subset such that where deno…- Let be a set, let denote the natural numbers, and let be a family of subsets of such that is nonempty for every . Then there exists a sequence in such that for every…
A Compact Subset of a Metric Space is Sequentially Compact
corollarycor:compact-implies-sequentially-compact-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 . Then is sequentially compact in .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…Existence of a Sequence of Positive Real Numbers with Limit Zero
lemmalem:positive-null-sequence-real-2026aAnalysisLet denote the real numbers, with the order of the ordered field and the additive identity of the underlying field; write to mean and . Then there exists a sequence in such that for every…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 Natural Numbers Are Well Ordered
theoremthm:well-ordering-natural-numbers-2026aNumber TheorySet TheoryLet denote the natural numbers with the order , and let be nonempty. Then has a least element: there exists such that for every . This element is unique, and is denoted .Strictly Increasing Sequences of Natural Numbers Dominate Their Index
lemmalem:subsequence-index-growth-2026aAnalysisSet TheoryLet denote the natural numbers with the addition of that definition and the order , and let be a sequence in that is strictly increasing in the sense of Subsequence of a Sequence in a Set. Then for every…- Let be a set, and let be a sequence in , indexed by the natural numbers carrying the addition of that definition and the order . A sequence in is strictly increasing if for every…
Approximation Property of the Supremum and the Infimum in
lemmalem:supremum-infimum-approximation-real-2026aAnalysisLet denote the real numbers, whose order is that of an ordered field and in particular a total order, and whose addition and additive inverses are those of the underlying field; write for , and write to mean that and . Let…Existence of the Infimum of a Nonempty Subset of Bounded Below
theoremthm:infimum-existence-real-2026aAnalysisLet denote the real numbers, whose order is that of an ordered field and in particular a total order. Let be nonempty and bounded below. Then has a greatest lower bound in . By…- Let be a set equipped with a total order , and let . Then has at most one least upper bound in , and at most one greatest lower bound in . Accordingly, when a least upper bound of exists it is denoted , and when a greatest lower bound…
Lower Bound and Greatest Lower Bound in a Totally Ordered Set
definitiondef:lower-bound-infimum-total-order-2026aAnalysisAlgebraLet be a set equipped with a total order , and let . An element is a lower bound for if for every . If such an exists, then is bounded below. An element is a greatest lower bound, or infimum, of if…Elementary Properties of the Minimum of Two Elements
lemmalem:minimum-two-elements-properties-2026aAlgebraLogicLet be a set equipped with a total order , let , let denote the minimum of and , and let denote their maximum. Then the following hold. 1. (Lower bound) and . 2. (Attainment)…Minimum of Two Elements of a Totally Ordered Set
definitiondef:minimum-two-elements-2026aAlgebraLogicLet be a set equipped with a total order , and let . The minimum of and , written , is the element of defined as follows: if , then is ; otherwise is .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…