The Cantor–Schröder–Bernstein Theorem for $$\infty $$-groupoids

We show that the Cantor–Schröder–Bernstein Theorem for homotopy types, or $$\infty $$ ∞ -groupoids, holds in the following form: For any two types, if each one is embedded into the other, then they are equivalent. The argument is developed in the language of homotopy type theory, or Voevodsky’s univalent foundations (HoTT/UF), and requires classical logic. It follows that the theorem holds in any boolean $$\infty $$ ∞ -topos.

A proof for Cantor-Schröder-Bernstein Theorem using the diagonal argument

We prove Cantor-Schröder-Bernstein theorem using the diagonal argument.

Input Pattern Classification Based on the Markov Property of the IMBT with Related Equations and Contingency Tables

In this contribution, we provide a detailed analysis of the search operation for the Interval Merging Binary Tree (IMBT), an efficient data structure proposed earlier to handle typical anomalies in the transmission of data packets. A framework is provided to decide under which conditions IMBT outperforms other data structures typically used in the field, as a function of the statistical characteristics of the commonly occurring anomalies in the arrival of data packets. We use in the modeling Bernstein theorem, Markov property, Fibonacci sequences, bipartite multi-graphs, and contingency tables.

On complete monotonicity of three parameter Mittag-Leffler function

Using the Bernstein theorem we prove the complete monotonicity of the three parameter Mittag?Leffler function E??,? (?w) for w ? 0 and suitably constrained parameters ?, ? and ?.

NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF

Natural Formalization proposes a concrete way of expanding proof theory from the meta-mathematical investigation of formal theories to an examination of “the concept of the specifically mathematical proof.” Formal proofs play a role for this examination in as much as they reflect the essential structure and systematic construction of mathematical proofs. We emphasize three crucial features of our formal inference mechanism: (1) the underlying logical calculus is built for reasoning with gaps and for providing strategic directions, (2) the mathematical frame is a definitional extension of Zermelo–Fraenkel set theory and has a hierarchically organized structure of concepts and operations, and (3) the construction of formal proofs is deeply connected to the frame through rules for definitions and lemmas. To bring these general ideas to life, we examine, as a case study, proofs of the Cantor–Bernstein Theorem that do not appeal to the principle of choice. A thorough analysis of the multitude of “different” informal proofs seems to reduce them to exactly one. The natural formalization confirms that there is one proof, but that it comes in two variants due to Dedekind and Zermelo, respectively. In this way it enhances the conceptual understanding of the represented informal proofs. The formal, computational work is carried out with the proof search system AProS that serves as a proof assistant and implements the above inference mechanism; it can be fully inspected at http://www.phil.cmu.edu/legacy/Proof_Site/. We must—that is my conviction—take the concept of the specifically mathematical proof as an object of investigation. Hilbert 1918