R5624: Euclidean real dot product is symmetric |

R4189: |

R4329: Probability of countable intersection with an almost sure event |

R3587: Random basic number almost surely finite iff positive and negative parts are |

R3869: Row-standardisation of row-independent random real standard triangular array |

R4469: Countable union of stationary measurable sets is stationary |

R4919: Measurable transformation preserves independent countable random collection |

R797: Principle of weak mathematical induction on the natural numbers |

R3215: Characteristic function of indicator random boolean number |

R5562: Characteristic polynomial for a lower triangular complex matrix |

R4369: Set of euclidean rational numbers has Lebesgue measure zero |

R5558: Characteristic polynomial for a complex diagonal matrix of constant diagonal |

R1170: Euclidean volume of singleton |

R4058: Boolean Cantor diagonal sequence is not a term in the sequence inducing it |

R5621: |

R2970: The four classes of real intervals are each closed under translation |

R3404: Bayes' theorem in the case of two events |

R5081: Complex matrix determinant zero iff some nonzero vector is mapped to zero |

R2436: Polar representation of complex conjugate |

R81: Bilipschitz map is continuous |

R1371: Bilinear map is zero if either argument is zero |

R1856: Cardinality of the set of maps between finite sets |

R982: Sequential continuity of measure from below |

R4693: Lower bound to the product of duals of a finite collection of real numbers in the left-closed unit interval |

R3738: Median need not be unique for a random real number |

R4844: Mutual information of a simple random variable with respect to itself |

R3513: Measurable subnull set has measure zero |

R5242: Finite sum of uncorrelated identically distributed Poisson random natural numbers is Poisson |

R4215: Countable set intersection is invariant under bijective shifting of indices |

R5126: Fundamental theorem of complex trigonometry |

R263: Binary cartesian product of countable sets is countable |

R4485: Convergent sequence in metric space has unique limit point |

R4333: Binary product of indicator functions equals indicator of intersection |

R4757: Young's inequality for two real numbers |

R4740: Upper bound to the probability that two finite random euclidean real sums equal each other |

R4141: Probabilistic Chernoff inequality |

R2950: Complex conjugation operation is an involution |

R4932: |

R4659: Empirical probability distribution function is an unbiased estimator of the true distribution function |

R5049: |

R4107: Determinant of real diagonal matrix with constant diagonal |

R4541: Open set is its own interior |

R5235: Sample mean of I.I.D. gaussian random real numbers is a gaussian random real number |

R5514: Determinant of a complex identity matrix |

R5482: Columns of a real identity matrix span the whole space |

R4695: An infinite product of real numbers on the open unit interval need not converge to zero |

R2690: Minimum and maximum of stopping times are stopping times |

R2310: Distribution formula for unsigned basic integral |

R3060: Riemann integral of even real function over an interval symmetric abour zero |

R4165: Superset of countable union iff superset of every set in the union |

R1275: Every map to trivial topological space is continuous |

R5511: Interchanging two rows or two columns of a real square matrix switches the sign of the determinant |

R4866: Generating a random real number with randomness from a standard uniform variable |

R4826: Logarithm of a ratio |

R4577: Countable indicator partition of complex expectation in terms of pullback events |

R5513: Real matrix determinant is homogeneous with respect to multiplying a row or a column by a constant |

R5524: Complex arithmetic expression for the determinant of a 3-by-3 complex square matrix |

R5575: Traces of complex matrix gramians coincide |

R4855: Reflection property of standard logarithm function |

R3384: Components of gaussian random euclidean real number are gaussian random basic real numbers |

R4825: Bit entropy of a standard bernoulli number is one bit |

R714: Element belongs to its own equivalence class |

R4607: Pushforward change of variables formula for unsigned basic integral |

R1165: Reflection invariance of Lebesgue measure |

R4782: Expectation of conditional expectation for a random real number |

R4470: Inverse image of countable union is union of inverse images |

R4996: |

R2338: Finite sum of I.I.D. exponential random positive real numbers is a gamma random random positive real number |

R3641: Conditional probability given independent random variable |

R2665: Characteristic function of gaussian random real number |

R1160: Reflection invariance of Euclidean volume function |

R2168: Isotonicity of Lebesgue outer measure |

R5544: Real matrix trace is preserved by transposing |

R2182: Isotonicity of real sublevel sets |

R5079: Characterisation of complex matrix eigenvalues in terms of characteristic polynomial |

R3518: Partition of random basic number into positive and negative parts |

R2929: Sum of odd functions is odd |

R75: Intersection of closed sets is closed |

R5322: Adding the same random real number need not preserve equality in distribution |

R24: Parallelogram identity |

R5525: Complex square matrix which has a zero column or a zero row has determinant zero |

R4055: Singleton map is injection from set to power set |

R1236: Markov's inequality |

R233: Whole space is closed |

R244: Convergent sequence is Cauchy |

R5183: Unique global maximizer for a finite product of unsigned real numbers with a given sum |

R2933: Isotonicity of countably infinite real summation |

R5324: Conditional expectation of a random real number conditioned on itself |

R4786: Real conditional covariance partition into conditional moments |

R4010: Polish space is first-countable |

R511: Natural number plane is countable |

R1338: Probabilistic Borel-Cantelli lemma |

R1077: Maximum element is unique |

R3988: Expression for quadratic form of real square matrix in terms of symmetric part |

R4781: Conditional expectation of known random real number |

R4876: Interval length upper bound to variance of bounded random real number |

R4912: Strong derivative for symmetric euclidean real quadratic form |

R4273: Absolute value function preserves zero |

R5284: Expectation of a Bernoulli random boolean number |

R5614: |

R4847: Probability of event conditional on itself |

R5185: Tight lower bound to a finite product of positive real numbers |

R3748: Finite real matrix is positive definite iff symmetric part is |

R1831: Real arithmetic expression for binomial coefficient |

R4349: Two disjoint events independent iff one is of probability zero |

R3719: Probability of complement event |

R4445: Inclusion-exclusion principle for probability of binary union |

R4631: Cardinality of finite cartesian products is invariant under insertion of parentheses |

R3783: Law of total probability for complex expectation in terms of pullback events |

R1577: Cauchy's theorem for a disc |

R2798: Moments of an indicator random boolean number |

R262: Countable union of countable sets is countable |

R4831: Homomorphism property of standard logarithm function |

R3904: Characteristic function of a Poisson random natural number |

R4947: Variance of standard Bernoulli random boolean number |

R508: Finite cartesian product of countable sets is countable |

R5559: Characteristic polynomial for a complex diagonal matrix |

R5561: Characteristic polynomial for an upper triangular complex matrix |

R7: Empty set is subset of every set |

R5283: Expectation of a standard bernoulli random boolean number |

R4611: |

R2748: Finite sets are closed in metric space |

R4597: Centred gaussian real density function is an even function |

R4777: Expectation of bounded random real number is within the bounding interval |

R3645: Countable partition additivity of unsigned basic measure |

R4830: Change of base formula for logarithm function |

R5563: Eigenvalue sequence for a triangular complex matrix |

R2897: Fourier transform under scaling |

R2677: Law of total probability for a countable partition of events of positive probability |

R2787: Pascal's rule |

R5168: Infinite product of real numbers in right-closed unit interval vanishes iff infinite sum of duals diverges |

R4998: Limit of distribution function of geometric random positive integer scaled by reciprocal of index |

R4687: Additivity of variance for a finite number of independent random real numbers |

R5362: Probability that a continuous random real number takes value in the rational numbers is zero |

R4143: Countable union is an upper bound to each set in the union |

R4928: Finite partition additivity of probability measure |

R4182: Isotonicity of sublevel probabilities for a random real number |

R1076: Minimum element is unique |

R5282: Expectation of a random fraction need not equal fraction of expectations |

R4049: Number of binary relations on a finite set |

R5190: Weighted Cauchy-Schwarz inequality for two real sequences |

R2588: Weak Stirling formula |

R4328: Probability of finite union with an almost sure event |

R4729: Complex binomial inequality |

R2060: Probability of set difference |

R4706: Complex conjugate zero iff argument zero |

R3516: Signed basic expectation of almost surely zero random number is zero |

R4261: Real binomial theorem for exponent two |

R4808: Affine transformations preserve independent real pairs |

R4118: Real arithmetic expression for unsigned real geometric mean |

R2754: Lipschitz map is Hölder continuous |

R2220: Binary set intersection is commutative |

R4186: Complement of a G-delta set is an F-sigma set |

R3646: Countable partition additivity of probability measure |

R4950: Real matrix with no real eigenvalues |

R4899: |

R3972: Expression for random basic real sum of squares in terms of sample mean and variance |

R5211: Tight upper bound to a product of three unsigned real numbers |

R315: Composition of surjections is surjection |

R4503: Countable union of sets of measure zero is of measure zero |

R4846: Conditional simple entropy with respect to itself |

R975: Isotonicity of unsigned basic measure |

R2876: Real mean value inequality |

R4483: Real number is zero iff equal to its reflection |

R5273: Finiteness of expectation in general does not imply finiteness of variance for random real number |

R5498: Inverse matrix is unique for real square matrix |

R2525: Independence of sigma-algebras is hereditary |

R4765: Reflection preserves euclidean real subset relation |

R5300: Unsigned basic integral over an empty set equals zero |

R4310: Number of N-ary relations on a finite set |

R4817: Data processing inequality for transformed endpoint |

R3670: Modulus sum upper bound to distance between two finite complex products for complex numbers in the unit disc |

R2089: Unsigned basic expectation is compatible with probability measure |

R2963: Odd function equals its odd part |

R4550: |

R5301: Random unsigned basic number has zero correlation with the empty indicator |

R3512: Unsigned basic integral over set of measure zero is zero |

R5576: Eigenvectors for a symmetric complex matrix are orthogonal |

R738: Left and right cosets coincide in Abelian group |

R4171: Difference of set and countable union equals intersection of differences |

R5285: Expectation of a gaussian random real number |

R4869: Characterisation of subconvex real functions |

R4873: |

R1177: Constant map is always measurable |

R4857: Standard logarithm of a positive real number raised to an integer power |

R4982: Exchangeable random collection is identically distributed |

R3583: Random basic number absolutisation equals sum of positive and negative parts |

R3544: Endpoint bounds for real arithmetic mean |

R4216: Finite set intersection is invariant under bijective shifting of indices |

R2090: Isotonicity of probability measure |

R4666: Real GM-HM inequality |

R5569: Determinant of reflected complex matrix |

R5189: |

R5070: Determinant of a diagonal complex matrix with constant diagonal |

R1064: Isotonicity of Lebesgue measure |

R1276: Every map from discrete topological space is continuous |

R716: Equivalence class is not empty |

R3945: Set is a superset to its interior |

R1158: Translation invariance of Euclidean volume function |

R1841: Indicator function operator is a bijection |

R4272: Absolute value function is not strictly antitone |

R3885: Gaussian approximation to Poisson distribution |

R26: Pythagorean theorem |

R5460: Sample variance is an unbiased estimator for the variance of I.I.D. random real numbers |

R2747: Finite sets are closed in Hausdorff space |

R976: Finite disjoint additivity of unsigned basic measure |

R2374: Borel-Cantelli zero-one law |

R4720: Conditional probability of complement event |

R979: Countable subadditivity of measure |

R4915: |

R354: Image of singleton set |

R4106: Determinant of real diagonal matrix |

R648: Proportionally bounded linear map is Lipschitz |

R5565: Eigenvalue sequence for a lower triangular complex matrix |

R4287: Finite product of even complex functions is even |

R5303: Real-linearity of complex expectation |

R2440: Translation invariance of Lebesgue outer measure |

R2556: Probability calculus expression for probability conditioned on event of nonzero probability |

R4913: Strong derivative for euclidean real quadratic form without translation |

R4095: Real arithmetic expression for real arithmetic mean |

R4639: Characteristic function for translated random real number |

R4500: |

R1232: Tonelli's theorem for sums and integrals |

R2410: I.I.D. real weak law of large numbers under finite second absolute moments |

R5393: I.I.D. real empirical distribution measure converges to a probability for a fixed Borel set |

R3259: Weak law of large numbers for variance with weighted decay |

R3232: Value of standard logarithm function at its parameter value |

R3200: Characteristic function of Bernoulli random boolean number |

R3649: Expectation of conditional probability |

R5162: Minimizer need not be unique for a subconvex real function |

R1959: Young's inequality |

R4188: Set cardinality in terms of finite ambient set |

R1846: Cardinality of set complement |

R5276: Probability to win an I.I.D. exponential race |

R2441: Reflection invariance of Lebesgue outer measure |

R3939: Upper and lower bounds for codomain set of finite unsigned basic measure |

R1557: Weighted real AM-GM inequality |

R5061: Expression for a real matrix inverse in terms of adjugate |

R80: Lipschitz map is continuous |

R1903: Basic integral of almost everywhere zero function is zero |

R3680: Characteristic function of standard gaussian random real number |

R4743: Riemann integral average of vanishing unsigned basic real function vanishes |

R3231: Riemann integral analogue to infinite geometric series |

R5169: Infinite product of real numbers in right-closed unit interval does not vanish iff infinite sum of duals converges |

R4948: Gaussian approximation to standard binomial distribution |

R4443: Measure of symmetric difference of set and subset |

R2160: Conditional expectation of known random complex number |

R3600: Finite sum of independent Poisson random natural numbers is Poisson |

R5104: Proof by principle of weak mathematical induction on the natural numbers |

R4649: Probability calculus expression for basic real conditional expectation given a countable partition of the sample space |

R1193: Finite product of indicator functions equals indicator of intersection |

R2091: Sequential continuity of probability measure from below |

R3938: Upper and lower bounds for codomain set of probability measure |

R978: Measure of set difference |

R4944: Real binomial theorem for exponent four |

R4468: Set of stationary measurable sets is a sigma-algebra |

R5531: Eigenvalue sequence exists for every complex square matrix |

R4926: Finite partition additivity of unsigned basic measure |

R4903: Strong derivative for affine basic real function |

R4455: |

R4330: Probability of finite intersection with an almost sure event |

R5622: |

R5564: Eigenvalue sequence for an upper triangular complex matrix |

R5073: Determinant of an upper triangular complex matrix |

R5170: Expectation of conditional expectation for a random complex number |

R2413: Complex conjugate of real number |

R4325: Probability one if conditional probability one relative to event of probability one |

R4131: Markov lower bound on unsigned basic expectation |

R5509: Cofactor partition for the determinant of a 3-by-3 real square matrix |

R5537: Derivative function for euclidean real self-dot product function |

R1159: Euclidean volume function under scaling |

R403: Square of the imaginary number |

R5520: Cofactor partition for a 2-by-2 complex square matrix |

R2223: Binary set union is commutative |

R5519: Real arithmetic expression for the determinant of a 2-by-2 real square matrix |

R5209: Of all rectangles with a given perimeter, the square maximizes the area |

R88: Convolution is associative |

R4512: |

R5526: Complex matrix determinant is homogeneous with respect to multiplying a row or a column by a constant |

R4901: Probability density function for standard exponential random positive real number |

R3833: Uncorrelated random collection need not be independent |

R2239: Expectation of exponential random positive real number |

R4739: Binary subadditivity of probability measure |

R5232: Finite sum of independent gaussian random real numbers is a gaussian random real number |

R4093: Real harmonic and arithmetic means are multiplicative inverses when arguments are |

R74: Finite union of closed sets is closed |

R4965: Relationship with the sum of initial natural numbers and the binomial coefficient |

R2802: Expectation of the absolute value of a centred gaussian random real number |

R2492: Independent event collection is pairwise independent |

R4583: |

R4794: Independent minimums preserve exponential distribution |

R5229: Bessel-corrected sample variance of independent standard gaussians is a transformed chi-squared random real number |

R5060: Product of a real square matrix and its adjugate is a constant diagonal matrix |

R2964: Even function equals its even part |

R2016: Probabilistic Markov's inequality |

R4601: Element in countable cartesian product iff components in images of canonical projections |

R3535: Riemann integral of unit semicircle |

R3954: Two almost surely equal random variables are identically distributed |

R4228: Real ordering is compatible with addition |

R2079: Isotonicity of set intersection |

R2764: Canonical singleton map is bijection |

R3517: Unsigned basic expectation zero iff random number almost surely zero |

R1083: Minimal element is minimum element in ordered set |

R2483: Variance of Bernoulli random boolean number |

R3626: Sample variance is an unbiased estimator for the variance of uncorrelated identically distributed random real numbers |

R4904: Derivative for real square function |

R2934: Isotonicity of unsigned basic real series |

R76: Empty set is closed |

R4841: Finite disjoint additivity of probability measure |

R5532: Complex matrix determinant equals product of eigenvalues |

R3228: Bounded sequence need not be Cauchy |

R5304: Complex-linearity of real expectation |

R2491: Pairwise independent event collection need not be independent |

R246: Cauchy sequence is bounded |

R4430: Probability of event in backward orbit under probability-preserving endomorphism |

R4391: Characteristic function uniquely identifies the distribution of a random euclidean real number |

R4916: |

R4660: Real empirical probability distribution function converges pointwise to the true distribution function |

R4906: |

R4309: Number of N-ary relations on a finite cartesian product |

R5141: Real log-sum-exp method |

R4898: |

R1406: Collection of sets ordered by inclusion contains a maximal element |

R4805: Dual probability distribution function for geometric random positive integer |

R4755: Inverse image of a reflected real set |

R517: Singletons are closed in Hausdorff space |

R2262: Real variance partition into first and second moments |

R1973: Map composition is associative |

R4920: Measurable transformation preserves independent finite random collection |

R4092: Real arithmetic expression for real harmonic mean |

R4148: Intersection is a lower bound to each set in the intersection |

R5068: Determinant of a scaled complex matrix |

R1818: Isotonicity of real expectation |

R4970: |

R5194: |

R1074: Rolle's theorem |

R4150: Finite intersection is a lower bound to each set in the intersection |

R5243: Finite sum of uncorrelated identically distributed exponential random positive real numbers is a gamma random random positive real number |

R5643: Cardinality of the set of bytes |

R4562: Basic integral over a set of measure zero is zero |

R5545: Trace of conjugate transpose equals conjugate of trace |

R4206: Basic real golden ratio is a root of a quadratic basic real polynomial |

R2074: Isotonicity of inverse image |

R755: Group centre is Abelian group |

R5631: Strong fundamental theorem of complex algebra for a quadratic complex polynomial |

R4291: Vector space always has an inclusion-maximal linearly independent set |

R5404: I.I.D. real central limit theorem |

R800: Proof by principle of weak mathematical induction |

R2966: Indicator function under scaling of the argument |

R5508: Real square matrix invertible iff determinant nonzero |

R4573: Complex expectation over a null event is zero |

R4057: The set of boolean standard sequences is uncountable |

R3611: |

R4827: Entropy of a standard bernoulli number |

R708: Reverse triangle inequality for metric |

R3912: Characteristic function of rademacher random integer |

R4172: Difference of set and finite union equals intersection of differences |

R1149: Every point in open set is an interior point |

R4972: Bias-variance partition of mean square error for a random real column matrix |

R4780: Real conditional expectation given independent sigma-algebra |

R4811: Markov chain triple iff endpoints conditionally independent |

R2757: Proper contraction map is continuous |

R1839: Cardinality of power set of a finite set |

R5192: Cauchy-Schwarz inequality for two real sequences |

R4609: |

R4374: Integral factorisation on a binary product of basic real lebesgue measure spaces |

R5059: Adjugate for a 2-by-2 real square matrix |

R4822: Conditional probability of the sample space |

R4788: |

R4341: Bayes' theorem in the case of two pullback events |

R4563: Complex integral over a set of measure zero is zero |

R270: Real arithmetic expression for sum of a finite real geometric sequence |

R4387: Characteristic function of standard Poisson random natural number |

R4149: Countable intersection is a lower bound to each set in the intersection |

R3507: Binary union of countable sets is countable |

R5500: Transpose of real matrix inverse is inverse to the transpose |

R2750: Fourier transform of finite unsigned euclidean real Borel measure is uniformly bounded |

R3921: Identically distributed random collection need not be stationary |

R3996: |

R5420: Minimum and maximum of stopping times are stopping times for random real process |

R5299: Complex conjugate of a binary sum equals sum of complex conjugates |

R3679: Standardised I.I.D. real central limit theorem with the identity index sequence |

R2938: Vanishing sequence is necessary but not sufficient for finiteness of real series |

R4073: Probability of union with the impossible event |

R4908: Strong derivative for affine euclidean real function |

R5123: |

R1120: Antitonicity of minimum |

R47: Set difference is subset of the minuend |

R2138: Translation invariance of unsigned basic Lebesgue integral |

R2259: Variance of a finite sum of random real numbers |

R1975: Measure of set in backward orbit under measure-preserving endomorphism |

R4925: Probability calculus expression for conditional probability given disjoint non-null partition |

R5111: Number of injections is proportional to number of subsets of given size |

R2367: Law of total variance |

R4390: Fourier transform characterises euclidean real probability measure |

R3955: Components of standard gaussian random euclidean real number are standard gaussian random basic real numbers |

R1369: Jensen's inequality for expectation |

R4902: Strong derivative for constant real function |

R5180: Tight upper bound to directional derivative |

R5097: Power set is isomorphic to a set of boolean functions |

R590: Square root of two is irrational |

R3589: Random basic number almost surely finite if first absolute moment is finite |

R5424: |

R1234: Borel-Cantelli lemma |

R2786: Complement property of binomial coefficient |

R4157: Superadditivity of power set |

R3582: Signed expectation finite iff absolutely integrable random basic number |

R4973: Bias-variance partition of mean square error for random basic real number |

R4591: Binary additivity of transpose for real matrices |

R4756: |

R5091: Lindeberg central limit theorem for a standard triangular array |

R248: Binary subadditivity of basic real square root function |

R5241: Finite sum of I.I.D. Poisson random natural numbers is Poisson |

R221: Cartesian product is not associative |

R1130: Intersection is largest lower bound |

R3844: Characteristic function of a scaled random real number |

R2959: Function even part is even |

R4705: Inner product with repeating argument is a real number |

R2405: Characteristic function uniquely identifies the distribution of a random real number |

R2092: Sequential continuity of probability measure from above |

R822: Group of prime order is cyclic |

R4318: Inclusion-exclusion principle for unsigned basic measure of binary union |

R3896: Idempotence of real expectation |

R2377: Almost sure convergence implies convergence in probability |

R4632: Cardinality of cartesian triple products is invariant under insertion of parentheses |

R1904: Isotonicity of finite real summation |

R4783: |

R1178: Continuous map is Borel measurable |

R5093: Total number of fixed-length sequences using a given number of labels |

R4900: |

R2767: Identity map is an injection |

R2928: Finite sum of even euclidean real functions is even |

R292: Union is smallest upper bound |

R3883: Row-standardisation of row-independent random real triangular array |

R4263: Countable cartesian product with empty set is empty |

R468: Lagrange's theorem |

R3908: Characteristic function of almost surely constant random euclidean real number |

R3204: Characteristic function of geometric random positive integer |

R4038: Product of two finite real sums |

R5210: Tight upper bound to a product of two unsigned real numbers |

R5567: Eigenvalue sequence for a diagonal complex matrix with constant diagonal |

R5086: Eigenvectors for a symmetric real matrix are orthogonal |

R5566: Eigenvalue sequence for a diagonal complex matrix |

R4567: Countable indicator partition of a random euclidean real number |

R3633: Bessel-corrected sample variance is an unbiased estimator for the variance of uncorrelated identically distributed random real numbers |

R4849: Symmetry of simple mutual information |

R5251: Exponential random positive real number is a gamma random positive real number |

R4167: Superset of binary union iff superset of both sets in the union |

R3941: Slope function for standard real gaussian density function |

R2343: Uncorrelated real weak law of large numbers |

R5502: Real conditional expectation with respect to a constant random real number |

R3545: Endpoint bounds for real convex combination |

R4602: Element in finite cartesian product iff components in images of canonical projections |

R678: Vector space of finite real matrices is isomorphic to a euclidean real vector space |

R4800: Number of injections from a finite set to itself |

R293: Open set less closed set is open |

R2463: Determinant of a real identity matrix |

R3601: Gaussian approximation to standard Poisson distribution |

R4314: Number of boolean functions on a finite set |

R4627: |

R4730: Riemann integral of a constant function on the closed unit interval |

R3640: Conditional probability given independent sigma-algebra |

R4473: Almost idempotency of conditional expectation of random complex number |

R4754: |

R5308: Multiplying by the same random real number need not preserve equality in distribution |

R4467: Empty set is a stationary measurable set |

R5399: Sample average of I.I.D. integrable random real numbers converges to expectation almost surely |

R3472: Maximum modulus principle |

R2641: Euclidean real martingale is constant in expectation |

R3531: Pointwise product with indicator function is lower bound for unsigned basic function |

R4213: Countable set union is invariant under bijective shifting of indices |

R1194: Indicator function with respect to set complement |

R1401: Orthogonality relation is a symmetric binary relation |

R1036: Power set is closed under complements |

R4845: Joint entropy formula for simple mutual information |

R1851: Cardinality of set of permutations on finite set |

R5144: Vanishing gradient identifies a minimizer for differentiable subconvex real function |

R3385: Standard approximating sequence for the natural exponential function |

R4340: Bayes' theorem in the case of event and complement |

R4012: Polish space is Hausdorff |

R4665: Weighted real GM-HM inequality |

R4971: |

R49: Isotonicity of subtracting same set |

R5379: Distribution of the real Wiener process at a given point is gaussian |

R3970: Measure of finite union finite iff measure of all sets in union finite |

R5174: Transpose of a product of two complex matrices |

R2093: Countable subadditivity of probability measure |

R3514: Unsigned basic expectation over set of probability zero is zero |

R4737: |

R2295: Unit increment property of the gamma function |

R4997: |

R4907: Strong derivative for constant euclidean real function |

R50: Set difference equals intersection with complement |

R5182: Tight upper bound to a finite product of unsigned real numbers |

R2653: Real conditional expectation is absolutely integrable |

R5560: Characteristic polynomial for a triangular complex matrix |

R3969: Measure of intersection finite if measure of at least one set finite |

R5359: Reflection property of simple relative entropy |

R102: Singletons are closed in a metric space |

R5046: Absolute moment inherits finiteness from greater exponents for random real number |

R5188: |

R4338: Conditional probability of almost surely true event |

R5193: Maximal value for a directional derivative at a point |

R4540: Inverse map is a bijection |

R2548: Constant map pulls back a bottom sigma-algebra |

R2203: Expectation of a Poisson random natural number |

R4787: |

R4836: Change of base formula for simple entropy |

R87: Convolution is commutative |

R5127: Fundamental theorem of real trigonometry |

R4929: Binary partition additivity of probability measure |

R2075: Image of empty set |

R3595: Probabilistic Tonelli's theorem |

R5554: Real matrix trace is commutation invariant for two real matrices |

R4595: Basic real calculus expression for moments of centred gaussian random basic real number |

R4292: Finite cartesian product of finite sets is finite |

R298: Identity map is continuous if topology on domain set is equal or stronger |

R1075: Basic real interior extremum theorem |

R5518: Complex arithmetic expression for the determinant of a 2-by-2 complex square matrix |

R4279: Explicit algebraic expression for elements of generated subgroup with singleton generator set |

R3201: Characteristic function of a binomial random natural number |

R4132: Strict version of probabilistic Markov inequality |

R1854: Cardinality of the set of injections between finite sets |

R3562: Real conditional variance partition into conditional moments |

R4895: Standard counting measure is a point-mass measure |

R2989: Unsigned basic Lebesgue integral under scaling |

R5238: Sample mean of uncorrelated identically distributed gaussian random real numbers is a gaussian random real number |

R2313: Expectation with dual probability distribution function |

R5234: Sample mean of independent gaussian random real numbers is a gaussian random real number |

R90: Complex function convolution is homogeneous to degree one |

R4267: Set intersection with empty set is empty |

R3863: Signed basic integral with respect to a point measure |

R4823: Conditional probability of the empty event |

R1370: Multilinear map is zero if any argument is zero |

R3770: Product of real 2-by-2 matrix with its transpose |

R3784: Law of total probability for complex expectation in terms of pullback events of a discrete random variable |

R4145: Binary union is an upper bound to both sets in the union |

R4534: |

R4262: Finite cartesian product with empty set is empty |

R5175: Derivative function for standard natural real logarithm function |

R4348: Two disjoint events are not necessarily independent |

R4791: Probability for two independent standard Bernoulli random boolean numbers to coincide |

R4732: |

R2589: Trivial factorial upper bound |

R3205: Probability mass function for geometric random positive integer |

R3506: Finite union of countable sets is countable |

R4638: Complex-linearity of complex matrix trace |

R4166: Superset of finite union iff superset of every set in the union |

R4007: Singletons are closed in Polish space |

R3568: Real AM-GM inequality |

R2071: Isotonicity of set union |

R4437: Complement of stationary measurable set is stationary |

R4930: |

R5336: Expectation of an indicator random boolean number |

R4637: |

R4315: Cardinality of a finite set raised to a finite power |

R1171: Isotonicity of Euclidean volume function |

R1164: Translation invariance of Lebesgue measure |

R5405: Standard I.I.D. real central limit theorem |

R1233: Finite additivity of unsigned basic integral |

R3529: Tautological pointwise inequality from indicator functions on sublevel sets |

R4832: Homomorphism property of standard logarithm function in the binary case |

R3401: Probability calculus expression for conditional expectation given disjoint non-null partition |

R4011: Polish space is second-countable |

R4542: Map is inverse to its inverse |

R5485: Columns of a real matrix need not span the whole space |

R4617: The standard mollifier integrates to one |

R5186: Unique global minimizer for a finite product of positive real numbers with a given sum of multiplicative inverses |

R4568: Countable indicator partition of a random complex number |

R4173: Difference of set and binary union equals intersection of differences |

R1012: Monotonicity of real limits |

R3493: Empirical distribution function converges in probability to the true distribution function |

R1762: Closed set less open set is closed |

R1166: Lebesgue measure under scaling |

R4290: Vector space always has a linearly independent subset |

R4009: Metrisable topological space is Fréchet |

R5160: Subconvex real function need not have a minimizer |

R4513: |

R2615: Empty set is cofinite within a finite set |

R4560: Probability of complement of a null event |

R5085: Eigenvalues of a symmetric real matrix are real-valued |

R4278: Expression for probability of event in terms of complement event |

R4543: Map inverse is invertible |

R4598: Standard gaussian real density function is an even function |

R3316: Pointwise limit of continuous functions need not be continuous |

R1034: Power set is closed under unions |

R4370: Set of euclidean natural numbers has Lebesgue measure zero |

R4802: Law of total probability for complement partition in terms of random variables |

R1564: Oriented complex curve integral of continuous function with a primitive on open set |

R4909: Derivative for euclidean real self-dot product function |

R4317: Inclusion-exclusion principle for unsigned basic measure of ternary union |

R4689: Probabilistic Cavalieri principle |

R301: Canonical identity map is an injection |

R10: Binary cartesian product with empty set is empty |

R1073: Mean value theorem |

R4871: Translation property of the standard real log-sum-exp function |

R5008: Random unsigned basic number almost surely finite if expectation is finite |

R2080: Union is upper bound for intersection |

R4277: Measure of measurable set complement |

R5074: Determinant of a lower triangular complex matrix |

R2164: Law of the excluded middle in probability calculus |

R4867: Initial sum of powers of two |

R3148: Sum of real telescoping series |

R5173: Transpose of a product of three complex matrices |

R4829: Base inversion property of standard natural logarithm function |

R4308: Map composition need not be commutative |

R4670: Real geometric mean is a right limit of basic real power means |

R5063: Cofactor partition for the determinant of a real square matrix |

R5323: Conditional expectation need not preserve equality in distribution |

R5556: Squared eigenvalue is an eigenvalue for the square of a complex matrix |

R4962: Characteristic polynomial for a complex identity matrix |

R5510: Real square matrix which has a zero column or a zero row has determinant zero |

R2875: Cauchy's real mean value theorem |

R4801: Probability mass function for cogeometric random basic natural number |

R5297: Complex conjugate of a product of two complex numbers |

R1372: Inner product is zero if either argument is zero |

R2746: Finite sets are closed in Fréchet space |

R4662: Signed basic expectation with respect to a point probability measure |

R2484: Moments of a Bernoulli random boolean number |

R893: Cyclic group is Abelian |

R425: Euler's formulas for a real variable |

R5376: Riemann integral of an exponential random positive real number density function |

R5619: |

R5172: Real binomial theorem for exponent seven |

R4326: Probability of binary union with almost sure event |

R4559: Probability of complement of an almost sure event |

R4945: Real binomial theorem for exponent five |

R5237: Finite sum of uncorrelated identically distributed gaussian random real numbers is a gaussian random real number |

R756: Abelian group iff centre is whole group |

R5591: Real matrix gramians are positive semidefinite |

R399: Injectivity is hereditary |

R4838: Sum rule for simple marginal probability |

R5505: Cofactor matrix for a 2-by-2 real square matrix |

R5165: Central limit theorem for I.I.D. sample mean series |

R4331: Probability of binary intersection with an almost sure event |

R4214: Finite set union is invariant under bijective shifting of indices |

R4927: Binary partition additivity of unsigned basic measure |

R3745: Real square matrix antisymmetric part is zero definite |

R1540: Affine map preserves convex sets in images |

R3757: Linearity of basic real matrix trace |

R4285: Standard natural real exponential function maps zero to one |

R457: Fréchet space iff singletons are closed |

R424: Euler's identity |

R5291: Complex conjugate of a complex eigenvalue of a real matrix is an eigenvalue |

R5171: Real binomial theorem for exponent six |

R4144: Finite union is an upper bound to each set in the union |

R2141: Reflection invariance of unsigned basic Lebesgue integral |

R371: Countable set iff injection to natural numbers |

R4741: Probabilistic Chebyshov's inequality for square function |

R5296: Complex conjugate of a product of two complex column matrices |

R3547: Expectation minimises second central moment for random real number |

R3260: Weak law of large numbers for random real triangular arrays |

R5266: Real calculus expression for distribution function of standard exponential random positive real number |

R3461: Holomorphic function with vanishing derivative on complex domain is constant |

R4673: Napier's constant equals a limit of products with factors nearing one |

R2062: Antitonicity of subtracting from the same set |

R5363: A continuous random real number is almost surely an irrational number |

R4804: Probability distribution function for geometric random positive integer |

R3618: Turning two unsigned real numbers into convex combination coefficients |

R3602: Gaussian approximation to binomial distribution |

R2986: Lebesgue outer measure under scaling |

R4327: Probability of countable union with an almost sure event |

R5094: Number of boolean functions on a boolean cartesian product |

R4151: Binary intersection is a lower bound to each set in the intersection |

R4013: Polish space is Fréchet |

R4174: Proper contraction has at most a single fixed point |

R5435: Expectation of a chi-squared random unsigned real number |

R5230: Bessel-corrected sample variance of I.I.D. gaussians is a transformed chi-squared random real number |

R5484: Columns of a real matrix which span the whole space need not be real-linearly independent |

R4931: |

R1566: Mean value theorem for Riemann integral |

R1544: Anova partition of orthogonal projection |

R5233: Finite sum of I.I.D. gaussian random real numbers is a gaussian random real number |

R5568: Eigenvalue sequence for an identity complex matrix |

R4630: Bijection between parenthesis-sliced cartesian triple products |

R5395: Factorization need not preserve equality in distribution |

R4684: I.I.D. weak law of large numbers for random real numbers |

R5197: Characterisation of natural real exponential function by a differential equation |

R5530: Determinant of a scaled real matrix |

R4814: Markov chain triple iff reverse is a Markov chain triple |

R4537: Inclusion of inverse image does not imply inclusion of image |

R4961: |

R1514: Isotonicity of signed basic integral |

R5471: Real square matrix invertible iff transpose is |

R2962: Characterisation of standard natural real exponential function by a differential equation |

R2100: Triangle inequality for signed basic expectation |

R4848: Probability of event conditional on complement |

R4596: Real calculus expression for moments of standard gaussian random real number |

R5431: Growth class for the expectation of the absolute value of the standard integer random walk |

R4048: Number of binary relations on binary cartesian product |

R3559: Probability of random real number taking value in right-closed interval |

R352: Inverse image of image |

R4610: |

R5115: Natural number factorial is an even number for numbers 2 or greater |

R2955: Reciprocal positive integer sequence converges to zero |

R347: Isotonicity of map image |

R2960: Function odd part is odd |

R4733: Conditional expectation of known random euclidean real number |

R2150: Expectation of conditional expectation for a random euclidean real number |

R4368: Set of euclidean integers has Lebesgue measure zero |

R4453: Probability of symmetric difference of event and subevent |

R1035: Power set is closed under intersections |

R3532: Tautological pointwise lower bound from indicator function on sublevel set |

R4943: Real binomial theorem for exponent three |

R4538: Inclusion of image does not imply inclusion of inverse image |

R4738: Finite subadditivity of probability measure |

R1868: Composition of indicator function with set endomorphism |

R4126: Almost surely bounded random complex number has all absolute moments finite |