
R463 
Law of the excluded middle is a propositional tautology 

R4962 
Characteristic polynomial for a complex identity matrix 

R4292 
Finite cartesian product of finite sets is finite 

R4931 


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

R5632 
Derivative function for a real matrix quadratic form 

R5070 
Determinant of a diagonal complex matrix with constant diagonal 

R1022 
Partition of basic function into positive and negative parts 

R4086 
Real arithmetic expressions for AND boolean logic gate 

R5175 
Derivative function for standard natural real logarithm function 

R3201 
Characteristic function of a binomial random natural number 

R2082 
Binary set union with empty set 

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

R5099 
Sum of initial cubed natural numbers 

R3547 
Expectation minimises second central moment for random real number 

R4675 
Standard real logarithm function grows linearly near 1 

R4467 
Empty set is a stationary measurable set 

R176 
Canonical set epimorphism is surjection 

R4672 
Firstdegree polynomial approximation for a standard natural basic real exponential function near zero 

R2966 
Indicator function under scaling of the argument 

R2505 
Real covariance partition into first moments 

R2093 
Countable subadditivity of probability measure 

R5483 
Columns of a real matrix span the whole space if reallinearly independent 

R4611 


R5094 
Number of boolean functions on a boolean cartesian product 

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

R978 
Measure of set difference 

R5260 
Slope function for standard natural real logarithm function 

R2811 
Distance between expectation and median of a random real number is no more than one standard deviation 

R3507 
Binary union of countable sets is countable 

R4657 
Probability calculus expression for conditional probability given a finite partition of the sample space 

R4271 
Absolute value function is not strictly isotone 

R4825 
Bit entropy of a standard bernoulli number is one bit 

R5366 
The standard Cantor set is standard Borel 

R5261 
Slope function for standard real sine function 

R2751 
Fourier transform of absolutely integrable function is bounded 

R2221 
Set intersection is invariant under bijective shifting of indices 

R1162 
Lebesgue sigmaalgebra is closed under reflections 

R4929 
Binary partition additivity of probability measure 

R3232 
Value of standard logarithm function at its parameter value 

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

R3921 
Identically distributed random collection need not be stationary 

R447 
Zorn's lemma 

R4788 


R3401 
Probability calculus expression for conditional expectation given disjoint nonnull partition 

R5136 
Minimax inequality 

R5465 
Known random complex number behaves like a constant in conditional expectation 

R5438 
Chi random unsigned real number coincides in distribution with euclidean length of a standard multivariate gaussian 

R3512 
Unsigned basic integral over set of measure zero is zero 

R3518 
Partition of random basic number into positive and negative parts 

R3058 
Integer powers of the imaginary number 

R4688 
Second moment upper bound to real variance 

R3432 
Standard I.I.D. law of the iterated logarithm 

R5188 


R24 
Parallelogram identity 

R4270 
Set union with empty set 

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

R4676 


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

R477 
Set finiteness is hereditary 

R5289 
Real arithmetic expression for the value of geometric mean of a telescroping fintie real sequence 

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

R4776 
Hoeffding's lemma 

R2370 
Real arithmetic expression for cardinality of countable set 

R4007 
Singletons are closed in Polish space 

R2960 
Function odd part is odd 

R1818 
Isotonicity of real expectation 

R2074 
Isotonicity of inverse image 

R4010 
Polish space is firstcountable 

R2744 
Square root of prime is irrational 

R4323 


R1202 
Dominated convergence theorem for signed basic integral 

R5484 
Columns of a real matrix which span the whole space need not be reallinearly independent 

R2343 
Uncorrelated real weak law of large numbers 

R4332 


R5174 
Transpose of a product of two complex matrices 

R4485 
Convergent sequence in metric space has unique limit point 

R1164 
Translation invariance of Lebesgue measure 

R2754 
Lipschitz map is Hölder continuous 

R2466 
Real matrix determinant is multiplicative 

R1502 
Complexlinearity of complex integral 

R2313 
Expectation with dual probability distribution function 

R4804 
Probability distribution function for geometric random positive integer 

R432 
Set of natural numbers is countable 

R5189 


R4500 


R4260 
Real square root function is strictly isotone 

R5447 
Growth rate of the expectation of the absolute value of a standard real Wiener process 

R4141 
Probabilistic Chernoff inequality 

R4263 
Countable cartesian product with empty set is empty 

R4174 
Proper contraction has at most a single fixed point 

R2929 
Sum of odd functions is odd 

R4845 
Joint entropy formula for simple mutual information 

R5591 
Real matrix gramians are positive semidefinite 

R4283 
Standard natural basic real logarithm function escapes to positive infinity at positive infinity 

R1530 
Inverse image preserves set difference 

R1149 
Every point in open set is an interior point 

R4172 
Difference of set and finite union equals intersection of differences 

R4013 
Polish space is Fréchet 

R4732 


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

R399 
Injectivity is hereditary 

R1089 
Characterisation of convergent sequences in metric space 

R2441 
Reflection invariance of Lebesgue outer measure 

R4087 
Real arithmetic expressions for OR boolean logic gate 

R4900 


R4972 
Biasvariance partition of mean square error for a random real column matrix 

R5086 
Eigenvectors for a symmetric real matrix are orthogonal 

R5412 


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

R4638 
Complexlinearity of complex matrix trace 

R5517 
Cofactor partition for a complex square matrix 

R4314 
Number of boolean functions on a finite set 

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

R4443 
Measure of symmetric difference of set and subset 

R1869 
Characterisation of equality of maps 

R4945 
Real binomial theorem for exponent five 

R4348 
Two disjoint events are not necessarily independent 

R3517 
Unsigned basic expectation zero iff random number almost surely zero 

R4847 
Probability of event conditional on itself 

R3944 
Open set iff equal to interior 

R5068 
Determinant of a scaled complex matrix 

R219 
Difference of set and intersection equals union of differences 

R5621 


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

R2367 
Law of total variance 

R3192 
I.I.D. sequence of standard gaussian random real numbers is standard gaussian random euclidean real number 

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

R3833 
Uncorrelated random collection need not be independent 

R2067 
Subtracting empty set from set 

R5424 


R3195 
Components of Gaussian random Euclidean number are independent iff uncorrelated 

R2485 
Expectation of geometric random basic positive integer 

R4702 


R4349 
Two disjoint events independent iff one is of probability zero 

R4163 
Subset of binary intersection iff subset of both sets in the intersection 

R1856 
Cardinality of the set of maps between finite sets 

R1232 
Tonelli's theorem for sums and integrals 

R4265 
Finite set intersection with empty set is empty 

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

R76 
Empty set is closed 

R2091 
Sequential continuity of probability measure from below 

R4060 
Appropriately parenthesised cartesian products are isomorphic 

R4567 
Countable indicator partition of a random euclidean real number 

R4920 
Measurable transformation preserves independent finite random collection 

R4131 
Markov lower bound on unsigned basic expectation 

R5524 
Complex arithmetic expression for the determinant of a 3by3 complex square matrix 

R4704 


R4049 
Number of binary relations on a finite set 

R4287 
Finite product of even complex functions is even 

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

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

R4591 
Binary additivity of transpose for real matrices 

R4538 
Inclusion of image does not imply inclusion of inverse image 

R2955 
Reciprocal positive integer sequence converges to zero 

R4899 


R2295 
Unit increment property of the gamma function 

R1214 
Isotonicity of unsigned basic integral 

R4317 
Inclusionexclusion principle for unsigned basic measure of ternary union 

R2014 
Triangle inequality for signed basic integral 

R3605 
Subadditivity of basic real square root function 

R4079 
Modus tollendo ponens in propositional logic 

R4463 
Strongly mixing probabilitypreserving system is weakly mixing 

R1650 
Interior point of set iff has open neighbourhood contained in set 

R3471 
Open complex mapping theorem 

R4444 
Superset differenced from set equals empty set 

R4836 
Change of base formula for simple entropy 

R797 
Principle of weak mathematical induction on the natural numbers 

R4559 
Probability of complement of an almost sure event 

R2407 
Measurable transformation preserves independence 

R4473 
Almost idempotency of conditional expectation of random complex number 

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

R5448 
Expectation of the absolute value of a standard real wiener process at a given point 

R5074 
Determinant of a lower triangular complex matrix 

R5529 
Complex matrix determinant is additive with respect to row or column addition 

R5534 
Complex matrix invertible iff every eigenvalue nonzero 

R5570 
Special coefficients of complex matrix characteristic polynomial 

R5166 
Series converges for real numbers in the leftclosed unit interval iff infinite product of duals does not vanish 

R4338 
Conditional probability of almost surely true event 

R4610 


R3633 
Besselcorrected sample variance is an unbiased estimator for the variance of uncorrelated identically distributed random real numbers 

R1160 
Reflection invariance of Euclidean volume function 

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

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

R1406 
Collection of sets ordered by inclusion contains a maximal element 

R3304 
Approximating sequence for the natural exponential function 

R4714 
Sufficient condition for the existence of density function for a random euclidean real number 

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

R3500 
Homomorphism property of the standard natural real exponential function 

R5442 
Variance of a standard gaussian random real number 

R3508 
Fermat's last theorem 

R4694 


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

R3416 
Absolute value bounds for a basic real number 

R3863 
Signed basic integral with respect to a point measure 

R4902 
Strong derivative for constant real function 

R4782 
Expectation of conditional expectation for a random real number 

R1070 
Extreme value theorem for basic real calculus 

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

R5045 
Real matrix multiplied by column matrix from the right 

R3844 
Characteristic function of a scaled random real number 

R4285 
Standard natural real exponential function maps zero to one 

R4669 
Diagonalizable complex matrix is symmetric 

R4308 
Map composition need not be commutative 

R4829 
Base inversion property of standard natural logarithm function 

R1076 
Minimum element is unique 

R2745 
The only subset of finite set with same cardinality is the ambient set itself 

R4173 
Difference of set and binary union equals intersection of differences 

R2168 
Isotonicity of Lebesgue outer measure 

R5124 
Modulus of complex number polar representation 

R5302 
Idempotence of complex expectation 

R3514 
Unsigned basic expectation over set of probability zero is zero 

R5135 
Derivative of the twodimensional softmax function 

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

R3582 
Signed expectation finite iff absolutely integrable random basic number 

R4873 


R4211 
Basic real golden ratio is limit of successive terms in the Fibonacci natural number sequence 

R5498 
Inverse matrix is unique for real square matrix 

R4171 
Difference of set and countable union equals intersection of differences 

R1577 
Cauchy's theorem for a disc 

R464 
Ex falso sequitur quodlibet 

R2092 
Sequential continuity of probability measure from above 

R1213 
Linearity of unsigned basic integral 

R3719 
Probability of complement event 

R5193 
Maximal value for a directional derivative at a point 

R4168 
Difference of set and countable intersection equals union of differences 

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

R3908 
Characteristic function of almost surely constant random euclidean real number 

R4580 
Empty set union equals the empty set 

R4289 
Vector space always has a basis 

R3649 
Expectation of conditional probability 

R2223 
Binary set union is commutative 

R3204 
Characteristic function of geometric random positive integer 

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

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

R3429 
Complex conjugation is a multiplicative operation 

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

R5180 
Tight upper bound to directional derivative 

R4834 


R1236 
Markov's inequality 

R3325 
Banach fixed point theorem 

R1372 
Inner product is zero if either argument is zero 

R5590 
Complex matrix gramians are positive semidefinite 

R2741 
Set equality iff inclusion in both directions 

R5409 
Expectation of the absolute value of a centred standard gaussian random real number 

R2060 
Probability of set difference 

R3869 
Rowstandardisation of rowindependent random real standard triangular array 

R4626 
Strict isotonicity of basic Riemann integral 

R3601 
Gaussian approximation to standard Poisson distribution 

R831 
Second group isomorphism theorem 

R3462 
Goursat's theorem for circles 

R4495 
Superconvex and superconvex basic real functions on open basic real interval are continuous 

R5176 
Cauchyschwarz inequality for real pairs 

R5319 
Conditional probabilities need not preserve equality in probability 

R3774 
Probability distribution function for exponential random positive real number 

R5063 
Cofactor partition for the determinant of a real square matrix 

R4264 
Cartesian product with empty set is empty 

R1903 
Basic integral of almost everywhere zero function is zero 

R4268 
Finite set union with empty set 

R4674 


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

R3885 
Gaussian approximation to Poisson distribution 

R5474 
Complex square matrix invertible iff conjugate transpose is 

R5080 
Complex matrix determinant nonzero iff kernel is trivial 

R4930 


R4266 
Countable set intersection with empty set is empty 

R2786 
Complement property of binomial coefficient 

R4800 
Number of injections from a finite set to itself 

R3404 
Bayes' theorem in the case of two events 

R221 
Cartesian product is not associative 

R3778 
Probability density function for exponential random positive real number 

R5091 
Lindeberg central limit theorem for a standard triangular array 

R1906 
Isotonicity of limits of real sequences 

R4309 
Number of Nary relations on a finite cartesian product 

R5595 
Positive definite complex square matrix is conjugate symmetric 

R1975 
Measure of set in backward orbit under measurepreserving endomorphism 

R716 
Equivalence class is not empty 

R5075 
Complex matrix determinant is multiplicative 

R4621 
Standard mollifier is an approximate identity for complex Lebesgue convolution 

R3586 
Basic function is finite almost everywhere iff positive and negative parts are 

R3166 
Fourier transform of absolutely integrable function vanishes at infinity 

R4925 
Probability calculus expression for conditional probability given disjoint nonnull partition 

R3262 
Dilations of unsigned tail probability converge to zero 

R4169 
Difference of set and finite intersection equals union of differences 

R4113 
Strong fundamental theorem of real algebra 

R237 
Intersection distributes over union 

R90 
Complex function convolution is homogeneous to degree one 

R2539 
Probabilistic Chebyshov's inequality 

R5142 
Subconvex real function iff firstorder Taylor approximates underestimates function globally 

R5201 
Real arithmetic expression for the value of a telescoping finite real product 

R4667 
Real function which is differentiable only at a single point 

R3971 
Intersection of sets of infinite measure need not have infinite measure 

R4887 
Cardinality of binary cartesian product of finite sets 

R1603 
De Moivre's theorem 

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

R2747 
Finite sets are closed in Hausdorff space 

R4598 
Standard gaussian real density function is an even function 

R3504 
Erdős discrepancy problem 

R4486 
Metric space is Hausdorff 

R4089 
Real arithmetic expressions for NAND boolean logic gate 

R1817 
Complexlinearity of complex expectation 

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

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

R1204 
Fatou's lemma for unsigned basic integral 

R2963 
Odd function equals its odd part 

R4770 
Inclusionexclusion lower bound to probability of binary intersection 

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

R3479 
Conformal complex function iff holomorphic bijection 

R2681 
Weak fundamental theorem of complex algebra 

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

R5577 
Complex matrix eigenvectors corresponding to distinct eigenvalues are linearly independent 

R4743 
Riemann integral average of vanishing unsigned basic real function vanishes 

R5323 
Conditional expectation need not preserve equality in distribution 

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

R4340 
Bayes' theorem in the case of event and complement 

R3789 
Absolute value strictly less than real number iff in symmetric open interval 

R4663 
Real square root function is superconvex 

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

R1841 
Indicator function operator is a bijection 

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

R5433 
Variance of the standard integer random walk after a given number of steps 

R5207 
Basel approximating sequence to Pi 

R355 
Inverse image of singleton set 

R5066 
Inverse of symmetric complex matrix is symmetric 

R5049 


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

R3412 
Euclidean real arithmetic mean minimises Euclidean distance 

R2491 
Pairwise independent event collection need not be independent 

R893 
Cyclic group is Abelian 

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

R4971 


R3832 
Mode maximizes expected number of correct guesses for a finite identically distributed sequence of discrete random real numbers 

R125 
Subset relation is reflexive 

R4618 
Riemann integral of standard basic real gaussian function on the real line 

R2150 
Expectation of conditional expectation for a random euclidean real number 

R5566 
Eigenvalue sequence for a diagonal complex matrix 

R4159 
Power set is not empty 

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

R1077 
Maximum element is unique 

R5509 
Cofactor partition for the determinant of a 3by3 real square matrix 

R5306 
Conditional expectation of a random complex matrix given minimal information 

R3559 
Probability of random real number taking value in rightclosed interval 

R88 
Convolution is associative 

R2138 
Translation invariance of unsigned basic Lebesgue integral 

R982 
Sequential continuity of measure from below 

R3562 
Real conditional variance partition into conditional moments 

R2261 
Variance of a Poisson random natural number 

R4456 


R3685 
Modulus sum upper bound to distance between two finite complex products 

R4543 
Map inverse is invertible 

R3652 
CramérWold theorem 

R4903 
Strong derivative for affine basic real function 

R25 
CauchySchwarz inequality 

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

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

R5545 
Trace of conjugate transpose equals conjugate of trace 

R4310 
Number of Nary relations on a finite set 

R4293 
Power set of a finite set is finite 

R4916 


R3748 
Finite real matrix is positive definite iff symmetric part is 

R4511 
Two complex numbers distinct iff difference distinct from zero 

R4583 


R2100 
Triangle inequality for signed basic expectation 

R2089 
Unsigned basic expectation is compatible with probability measure 

R5514 
Determinant of a complex identity matrix 

R4909 
Derivative for euclidean real selfdot product function 

R5050 
Derivative for real matrix function quadratic form 

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

R2950 
Complex conjugation operation is an involution 

R4747 


R5508 
Real square matrix invertible iff determinant nonzero 

R4139 
Mill's inequalities 

R3953 
Two almost surely equal random real numbers are identically distributed 

R3506 
Finite union of countable sets is countable 

R2799 
Variance of an indicator random boolean number 

R560 
Division theorem in the ring of basic integers 

R5255 
Slope function for pointwise product of two differentiable real functions 

R26 
Pythagorean theorem 

R2690 
Minimum and maximum of stopping times are stopping times 

R468 
Lagrange's theorem 

R1450 
Explicit algebraic expression for elements of generated subgroup 

R4125 
Two random real numbers identical in distribution have identical absolute moments 

R1487 
Ring is a subring of itself 

R4383 
Euclidean real Fourier transform is uniformly bounded 

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

R5500 
Transpose of real matrix inverse is inverse to the transpose 

R5563 
Eigenvalue sequence for a triangular complex matrix 

R370 
Countable set iff surjection from natural numbers 

R5369 
Shannon entropy of a geometric random positive integer 

R4042 
Rearrangement inequality for finite real summation 

R5378 
Distribution of the standard real Wiener process at a given point is gaussian 

R5085 
Eigenvalues of a symmetric real matrix are realvalued 

R5636 
Derivative function for a real matrix trace function 

R5259 
Slope function for pointwise sum of two differentiable real functions 

R5561 
Characteristic polynomial for an upper triangular complex matrix 

R5564 
Eigenvalue sequence for an upper triangular complex matrix 

R517 
Singletons are closed in Hausdorff space 

R4692 
Series diverges for real numbers in the leftclosed unit interval iff infinite product of duals vanishes 

R2164 
Law of the excluded middle in probability calculus 

R2589 
Trivial factorial upper bound 

R4550 


R5562 
Characteristic polynomial for a lower triangular complex matrix 

R3568 
Real AMGM inequality 

R3935 
Superset iff equal to union with subset 

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

R4092 
Real arithmetic expression for real harmonic mean 

R263 
Binary cartesian product of countable sets is countable 

R5416 


R3738 
Median need not be unique for a random real number 

R4801 
Probability mass function for cogeometric random basic natural number 

R2422 
Complexlinearity of Fourier transform 

R4754 


R4118 
Real arithmetic expression for unsigned real geometric mean 

R2224 
Set union is associative 

R5552 
Complex matrix trace is commutation invariant for two complex matrices 

R249 
CauchySchwarz inequality for finite real sequences 

R5575 
Traces of complex matrix gramians coincide 

R2411 
Characteristic function of exponential random positive real number 

R1514 
Isotonicity of signed basic integral 

R4540 
Inverse map is a bijection 

R4228 
Real ordering is compatible with addition 

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

R981 
Countably infinite measurable cover has measurable subcover 

R3923 
Standard gaussian random real number is symmetric about zero 

R2353 
Volume of an open ball in Euclidean space 

R220 
Difference of set and union equals intersection of differences 

R2732 
Kolmogorov zeroone law 

R2740 
Splitting a Riemann integral over an implicit interval partition 

R4764 


R4919 
Measurable transformation preserves independent countable random collection 

R4991 
Complex matrix multiplied from the right by a diagonal matrix 

R5254 
Slope function for standard natural real exponential function 

R5459 
Sample mean of identically distributed random real numbers is an unbiased estimator for expectation 

R3676 
Characteristic function for sum of independent random euclidean real numbers 

R2788 
Real binomial theorem 

R4290 
Vector space always has a linearly independent subset 

R5262 
Slope function for standard real cosine function 

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

R4701 


R5497 
Inverse matrix is unique for complex square matrix 

R4277 
Measure of measurable set complement 

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

R5272 
Reciprocal real function on on the positive reals is antitone 

R4703 


R4262 
Finite cartesian product with empty set is empty 

R2588 
Weak Stirling formula 

R2656 
De MoivreLaplace theorem 

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

R4808 
Affine transformations preserve independent real pairs 

R4604 
Density partition for natural number moment of a random real number 

R4039 
Product of two finite real sums with equal number of summands 

R4368 
Set of euclidean integers has Lebesgue measure zero 

R1275 
Every map to trivial topological space is continuous 

R2757 
Proper contraction map is continuous 

R1012 
Monotonicity of real limits 

R4817 
Data processing inequality for transformed endpoint 

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

R5197 
Characterisation of natural real exponential function by a differential equation 

R2986 
Lebesgue outer measure under scaling 

R1744 
Finite union of finite sets is finite 

R3747 
Transpose of finite product of real matrices 

R4827 
Entropy of a standard bernoulli number 

R2535 
Chebyshov's inequality 

R1566 
Mean value theorem for Riemann integral 

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

R4509 
Two real numbers distinct iff difference distinct from zero 

R2158 
Conditional expectation given independent sigmaalgebra 

R5231 
Sample mean of uncorrelated gaussian random real numbers is a gaussian random real number 

R4737 


R4926 
Finite partition additivity of unsigned basic measure 

R4090 
Real arithmetic expressions for XOR boolean logic gate 

R4698 
Unsigned basic integral with respect to a point measure 

R3206 
Probability mass function for binomial random natural number 

R5594 
Positive definite real matrix need not be symmetric 

R2615 
Empty set is cofinite within a finite set 

R2062 
Antitonicity of subtracting from the same set 

R4729 
Complex binomial inequality 

R5284 
Expectation of a Bernoulli random boolean number 

R246 
Cauchy sequence is bounded 

R1959 
Young's inequality 

R5139 
Expectation preserves random real number stochastic ordering relation 

R5009 
Bernoulli random boolean integer from a uniform random real number 

R5507 
Real square matrix invertible iff determinant is 

R1074 
Rolle's theorem 

R5147 
Reflection of standard natural real logarithm function is subconvex 

R4843 
Conditional entropy formula for simple mutual information 

R3424 
Complex exponential function preserves complex conjugation 

R5419 
Wald's first equation 

R4275 
Absolute value function is an even basic real function 

R2080 
Union is upper bound for intersection 

R5340 
Meanmedianmode inequality for a gaussian random real number 

R4849 
Symmetry of simple mutual information 

R425 
Euler's formulas for a real variable 

R4369 
Set of euclidean rational numbers has Lebesgue measure zero 

R5245 
Euclidean real number is zero iff equal to its reflection 

R4997 


R4502 
Difference of almost everywhere equal euclidean complex functions is almost everywhere zero 

R4755 
Inverse image of a reflected real set 

R5585 
Invertible complex matrix need not be diagonalizable 

R4328 
Probability of finite union with an almost sure event 

R1170 
Euclidean volume of singleton 

R1276 
Every map from discrete topological space is continuous 

R3385 
Standard approximating sequence for the natural exponential function 

R4693 
Lower bound to the product of duals of a finite collection of real numbers in the leftclosed unit interval 

R4088 
Peirce basic boolean logic gate iff complement of maximum function on basic boolean ordered pairs 

R4875 
Popoviciu's inequality 

R3904 
Characteristic function of a Poisson random natural number 

R3231 
Riemann integral analogue to infinite geometric series 

R3954 
Two almost surely equal random variables are identically distributed 

R4162 
Subset of finite intersection iff subset of every set in the intersection 

R4329 
Probability of countable intersection with an almost sure event 

R3598 
Wald's first equation under independence 

R4562 
Basic integral over a set of measure zero is zero 

R648 
Proportionally bounded linear map is Lipschitz 

R4091 
Biconditional boolean logic gate iff complement of trivial distance function on basic boolean ordered pairs 

R5126 
Fundamental theorem of complex trigonometry 

R1159 
Euclidean volume function under scaling 

R3529 
Tautological pointwise inequality from indicator functions on sublevel sets 

R3984 
Subcollection of independent random collection is independent 

R4796 
Probability for two independent exponential random positive real numbers to be smaller than the other 

R3032 
Set of real numbers is uncountable 

R4774 


R1178 
Continuous map is Borel measurable 

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

R2016 
Probabilistic Markov's inequality 

R4615 
Sufficient conditions to qualify as an approximate identity to complex Lebesgue convolution 

R4370 
Set of euclidean natural numbers has Lebesgue measure zero 

R3843 
I.I.D. real central limit theorem with the identity index sequence 

R1488 
Group is a subgroup of itself 

R4142 
Union is an upper bound to each set in the union 

R2464 
Determinant is preserved under transpose of complex matrix 

R4627 


R4466 
Whole space is a stationary measurable set 

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

R1904 
Isotonicity of finite real summation 

R2270 
Sigmaalgebra is closed under symmetric differences 

R5256 
Slope function for composition of two differentiable real functions 

R5614 


R3645 
Countable partition additivity of unsigned basic measure 

R5357 
An uncountable set can have Lebesgue measure zero 

R4637 


R4170 
Difference of set and binary intersection equals union of differences 

R2653 
Real conditional expectation is absolutely integrable 

R2641 
Euclidean real martingale is constant in expectation 

R4606 
Stieltjes integral calculus expression for natural number moment of a random real number 

R3695 
Standardised Lindeberg central limit theorem 

R2337 
Density function for binary sum of independent random basic real numbers 

R2954 
Standard real harmonic series diverges 

R2975 
Lebesgue sigmaalgebra is closed under reflections, translations, and scaling 

R4908 
Strong derivative for affine euclidean real function 

R112 
Cavalieri principle 

R3494 
GlivenkoCantelli theorem 

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

R3215 
Characteristic function of indicator random boolean number 

R5190 
Weighted CauchySchwarz inequality for two real sequences 

R5296 
Complex conjugate of a product of two complex column matrices 

R49 
Isotonicity of subtracting same set 

R4320 
Set of singletons is subset of power set 

R5329 
Real arithmetic expression for ReLU function in terms of the maximum operation 

R5531 
Eigenvalue sequence exists for every complex square matrix 

R2783 
Arithmetic expression for sum of initial squared natural numbers 

R4648 
Union of sigmaalgebras need not be a sigmaalgebra 

R4805 
Dual probability distribution function for geometric random positive integer 

R4464 


R4152 


R5305 
Conditional expectation of a random complex matrix given maximal information 

R2833 
Nonempty set is singleton iff all elements equal each other 

R3259 
Weak law of large numbers for variance with weighted decay 

R3960 
Identically distributed random variables need not be almost surely equal 

R5350 
Differential Shannon entropy of a uniform random real number 

R4992 
Complex matrix multiplied from the left by a diagonal matrix 

R5415 
Variance of a gamma random positive real number 

R2090 
Isotonicity of probability measure 

R4738 
Finite subadditivity of probability measure 

R233 
Whole space is closed 

R3498 
Homomorphism property of the standard natural logarithm 

R2222 
Set union is invariant under bijective shifting of indices 

R3920 
Sublevel events do not necessarily coincide for identically distributed random variables 

R2377 
Almost sure convergence implies convergence in probability 

R5414 
Expectation of a gamma random positive real number 

R1854 
Cardinality of the set of injections between finite sets 

R4536 
Map image empty iff underlying set empty 

R2483 
Variance of Bernoulli random boolean number 

R4106 
Determinant of real diagonal matrix 

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

R4748 


R714 
Element belongs to its own equivalence class 

R4009 
Metrisable topological space is Fréchet 

R5504 
Constant random variable pulls back a bottom sigmaalgebra 

R5230 
Besselcorrected sample variance of I.I.D. gaussians is a transformed chisquared random real number 

R3896 
Idempotence of real expectation 

R3440 
Uniformly continuous map preserves Cauchy sequences 

R5173 
Transpose of a product of three complex matrices 

R4763 
Set complement of map inverse image 

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

R2492 
Independent event collection is pairwise independent 

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

R368 
Image of countable set is countable 

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

R5208 
Sum of initial cubed natural numbers equals sum of initial natural numbers squared 

R4838 
Sum rule for simple marginal probability 

R3515 
Unsigned basic integral zero iff function almost everywhere zero 

R5119 
Binary homomorphism property of standard natural complex exponential function 

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

R977 
Ambient set is union of subset and complement of subset 

R5172 
Real binomial theorem for exponent seven 

R2506 
Independent random real collection is uncorrelated 

R309 
Leftinvertible map iff injection 

R2302 
Memorylessness property of exponential random positive real number 

R5303 
Reallinearity of complex expectation 

R268 
Basel problem 

R3415 
Necessary and sufficient conditions for convergence of geometric complex series 

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

R2972 
The four classes of real intervals are each closed under dilation 

R2876 
Real mean value inequality 

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

R4213 
Countable set union is invariant under bijective shifting of indices 

R2914 
CantorBernstein theorem 

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

R4541 
Open set is its own interior 

R5129 
Standard complex cosine function expressed in terms of complex exponential function 

R5348 
Differential Shannon entropy for a gaussian random real number 

R2780 
Upper bound for number of arrows in finite digraph 

R5285 
Expectation of a gaussian random real number 

R3942 
Derivative of gaussian basic real density function 

R590 
Square root of two is irrational 

R4769 


R2525 
Independence of sigmaalgebras is hereditary 

R3901 
Domain of map to monoid equals union of kernel and support 

R2798 
Moments of an indicator random boolean number 

R4848 
Probability of event conditional on complement 

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

R3974 
Sum of independedent standard chisquard random real numbers is chisquared 

R2386 
Characterisation of almost sure convergence using limit superior and limit inferior 

R1036 
Power set is closed under complements 

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

R4128 
Two random real numbers identical in distribution have identical moments 

R4671 
Firstdegree polynomial approximation for a standard basic real exponential function near zero 

R5263 
Slope function for standard real tangent function 

R4438 
Equivalent characterisations of ergodicity for probabilitypreserving system 

R4453 
Probability of symmetric difference of event and subevent 

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

R5482 
Columns of a real identity matrix span the whole space 

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

R5320 
Absolute value function preserves equality in distribution for random real numbers 

R4767 


R5370 
Geometric random positive integer is the maximum Shannon entropy random positive integer for a given expectation 

R4607 
Pushforward change of variables formula for unsigned basic integral 

R102 
Singletons are closed in a metric space 

R255 
Power set of empty set 

R4662 
Signed basic expectation with respect to a point probability measure 

R4387 
Characteristic function of standard Poisson random natural number 

R708 
Reverse triangle inequality for metric 

R5408 
I.I.D. real strong law of large numbers 

R5160 
Subconvex real function need not have a minimizer 

R822 
Group of prime order is cyclic 

R4513 


R4470 
Inverse image of countable union is union of inverse images 

R4350 
Finite superadditivity of finite set cardinality 

R5128 
Standard complex sine function expressed in terms of complex exponential function 

R4757 
Young's inequality for two real numbers 

R5576 
Eigenvectors for a symmetric complex matrix are orthogonal 

R3581 
Absolute moment inherits finiteness from greater exponents for random complex number 

R4273 
Absolute value function preserves zero 

R5418 
Counterexample to Wald's first equation when independence not satisfied 

R4331 
Probability of binary intersection with an almost sure event 

R4871 
Translation property of the standard real logsumexp function 

R4811 
Markov chain triple iff endpoints conditionally independent 

R4869 
Characterisation of subconvex real functions 

R47 
Set difference is subset of the minuend 

R4011 
Polish space is secondcountable 

R2373 
Second probabilistic BorelCantelli lemma 

R1885 
Absolute value of basic function equals sum of positive and negative parts 

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

R1868 
Composition of indicator function with set endomorphism 

R3681 
Meandeviance standardisation of a random real number 

R4012 
Polish space is Hausdorff 

R5520 
Cofactor partition for a 2by2 complex square matrix 

R3544 
Endpoint bounds for real arithmetic mean 

R4483 
Real number is zero iff equal to its reflection 

R5549 
Complex matrix gramians are conjugate symmetric 

R4947 
Variance of standard Bernoulli random boolean number 

R1075 
Basic real interior extremum theorem 

R1960 
Characterisation of measurepreserving transformations by signed integral 

R5364 
A finite real set is standard Borel 

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

R5571 
Complex algebra expression for the characteristic polynomial of a 2by2 complex square matrix 

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

R5171 
Real binomial theorem for exponent six 

R3261 
Probability for two independent Bernoulli random numbers to coincide 

R2665 
Characteristic function of gaussian random real number 

R4934 
Real conditional expectation given maximal information 

R2497 
Reflection property of the standard Wiener process 

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

R2120 
Bounded continuous function is Riemann integrable on a real interval 

R4274 
Absolute value function escapes to positive infinity in both directions 

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

R4147 
Not all subsets of a cartesian product need be cylinder sets 

R4898 


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

R10 
Binary cartesian product with empty set is empty 

R4948 
Gaussian approximation to standard binomial distribution 

R4888 
Isotonicity of set cardinality 

R4326 
Probability of binary union with almost sure event 

R3680 
Characteristic function of standard gaussian random real number 

R4982 
Exchangeable random collection is identically distributed 

R3996 


R5622 


R4215 
Countable set intersection is invariant under bijective shifting of indices 

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

R3958 
Intersecting subtrahend with minuend preserves set difference 

R4097 
Real arithmetic expression for real matrix determinant 

R4183 
Alternative basic real arithmetic expressions for Catalan sequence 

R3595 
Probabilistic Tonelli's theorem 

R5487 
Dimension of a vector space of finite real matrices 

R4566 
Countable indicator partition of a complex function 

R983 
Sequential continuity of measure from above 

R3956 
Expectation of random unsigned basic number by integrating tail probabilities 

R4654 
Probability calculus expression for basic real conditional expectation given a complement partition of the sample space 

R5092 
Probability of binary intersection with a null event 

R457 
Fréchet space iff singletons are closed 

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

R5162 
Minimizer need not be unique for a subconvex real function 

R3289 
Sequence in product space is Cauchy iff each component sequence is Cauchy 

R4996 


R4823 
Conditional probability of the empty event 

R2680 
The Quadratic Formula 

R4851 
Tight upper bound to simple entropy 

R4661 
Integer power recurrence of basic real golden ratio 

R3646 
Countable partition additivity of probability measure 

R5170 
Expectation of conditional expectation for a random complex number 

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

R4333 
Binary product of indicator functions equals indicator of intersection 

R5532 
Complex matrix determinant equals product of eigenvalues 

R431 
Set of integers is countable 

R3945 
Set is a superset to its interior 

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

R4921 
Affine transformations preserve independent countable real collection 

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

R3983 
Subcollection of independent collection of sigmaalgebras is independent 

R315 
Composition of surjections is surjection 

R2203 
Expectation of a Poisson random natural number 

R4639 
Characteristic function for translated random real number 

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

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

R3776 
Probability to win an exponential race 

R3946 
Interior is an open set 

R3148 
Sum of real telescoping series 

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

R4318 
Inclusionexclusion principle for unsigned basic measure of binary union 

R4915 


R4188 
Set cardinality in terms of finite ambient set 

R1131 
Image of inverse image 

R4295 
Power set of a countable set need not be countable 

R2687 
Approximating function for the natural exponential function 

R2034 
Weighted Hölder's inequality for real power means in the case of two real sequences 

R4520 
Complex conditional expectation is absolutely integrable 

R1130 
Intersection is largest lower bound 

R3770 
Product of real 2by2 matrix with its transpose 

R4780 
Real conditional expectation given independent sigmaalgebra 

R7 
Empty set is subset of every set 

R4867 
Initial sum of powers of two 

R4261 
Real binomial theorem for exponent two 

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

R2767 
Identity map is an injection 

R3873 
Expectation of stopping time for I.I.D. sum of standard uniform random basic real numbers 

R1035 
Power set is closed under intersections 

R4830 
Change of base formula for logarithm function 

R4445 
Inclusionexclusion principle for probability of binary union 

R3228 
Bounded sequence need not be Cauchy 

R1540 
Affine map preserves convex sets in images 

R4679 
Independent countable random real collection is uncorrelated 

R3612 
Standard natural basic real logarithm function is strictly isotone 

R4140 
Standardised Mill's inequalities 

R2239 
Expectation of exponential random positive real number 

R5102 
Count of boolean functions on initial positive integers with given sum 

R322 
Image of projection map 

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

R4534 


R3898 
Distribution of sum of two random euclidean real numbers is convolution of distribution measures 

R108 
Inclusion iff reverse inclusion of complements 

R4895 
Standard counting measure is a pointmass measure 

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

R2719 
Affine majorant for the standard natural logarithm 

R5537 
Derivative function for euclidean real selfdot product function 

R3205 
Probability mass function for geometric random positive integer 

R5318 
Unions need not preserve equality in probabilities for events 

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

R4437 
Complement of stationary measurable set is stationary 

R1851 
Cardinality of set of permutations on finite set 

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

R3912 
Characteristic function of rademacher random integer 

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

R371 
Countable set iff injection to natural numbers 

R4286 
Standard natural basic real logarithm function maps one to zero 

R4656 
Probability calculus expression for conditional probability given a countable partition of the sample space 

R4276 
Triangle inequality for absolute value function 

R3919 
Probability measure need not be an injection 

R1171 
Isotonicity of Euclidean volume function 

R4699 


R2259 
Variance of a finite sum of random real numbers 

R4304 
Nonempty finite poset contains a minimal element 

R3611 


R2989 
Unsigned basic Lebesgue integral under scaling 

R4327 
Probability of countable union with an almost sure event 

R1838 
Cardinality of finite set union of finite sets 

R5283 
Expectation of a standard bernoulli random boolean number 

R4746 
Superadditivity and subadditivity of limit superior and limit inferior for unsigned basic integral 

R2897 
Fourier transform under scaling 

R5325 
Conditional expectation of random real number conditioned on an independent random real number 

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

R5298 
Complex conjugatation is an additive operation 

R5586 
Diagonalizable complex matrix need not be invertible 

R4431 


R4794 
Independent minimums preserve exponential distribution 

R5533 
Complex matrix trace equals sum of eigenvalues 

R1565 
Goursat's theorem 

R4913 
Strong derivative for euclidean real quadratic form without translation 

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

R1743 
Intersection of finite sets is finite 

R2748 
Finite sets are closed in metric space 

R5506 
Inverse for a 2by2 real square matrix 

R5359 
Reflection property of simple relative entropy 

R4756 


R5229 
Besselcorrected sample variance of independent standard gaussians is a transformed chisquared random real number 

R4593 
Expectation of a standard gaussian random real number 

R17 
Bijection from the set of natural numbers to the set of integers 

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

R4932 


R3642 
Law of total probability for complement partition 

R1234 
BorelCantelli lemma 

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

R2437 
Euclidean real Fourier inversion theorem 

R5079 
Characterisation of complex matrix eigenvalues in terms of characteristic polynomial 

R403 
Square of the imaginary number 

R310 
Rightinvertible map iff surjection 

R1064 
Isotonicity of Lebesgue measure 

R5127 
Fundamental theorem of real trigonometry 

R5072 
Determinant of a triangular complex matrix 

R975 
Isotonicity of unsigned basic measure 

R5400 
Lévy characterisation of the standard real Wiener process 

R2141 
Reflection invariance of unsigned basic Lebesgue integral 

R5394 
Finite summation need not preserve equality in distribution 

R1544 
Anova partition of orthogonal projection 

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

R3745 
Real square matrix antisymmetric part is zero definite 

R3183 
First fundamental theorem of Riemann integral calculus 

R3198 
Finite sum of uncorrelated Poisson random natural numbers is Poisson 

R4269 
Countable set union with empty set 

R800 
Proof by principle of weak mathematical induction 

R4728 


R1193 
Finite product of indicator functions equals indicator of intersection 

R4303 
Nonempty finite poset contains a maximal element 

R4680 
I.I.D. strong law of large numbers for random real numbers of finite fourth moments 

R30 
Inverse image of intersection is intersection of inverse images 

R4809 
Affine transformations preserve independent finite real collection 

R2219 
Set intersection is associative 

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

R4214 
Finite set union is invariant under bijective shifting of indices 

R4904 
Derivative for real square function 

R4512 


R1832 
Cardinality of a finite cartesian product of finite sets 

R5623 
Euclidean complex dot product is conjugate symmetric 

R4928 
Finite partition additivity of probability measure 

R508 
Finite cartesian product of countable sets is countable 

R4455 


R4711 
Probability of complement of event which is not the whole sample space need not be nonzero 

R3513 
Measurable subnull set has measure zero 

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

R1902 
Signed basic integral of almost everywhere equal functions 

R2875 
Cauchy's real mean value theorem 

R1233 
Finite additivity of unsigned basic integral 

R4272 
Absolute value function is not strictly antitone 

R2086 
Finite inclusionexclusion principle for unsigned basic measure 

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

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

R5097 
Power set is isomorphic to a set of boolean functions 

R4720 
Conditional probability of complement event 

R2537 
Real exponentiation function with positive exponent is strictly isotone on positive reals 

R3020 
Complex Lebesgue integral under scaling 

R5360 
Probability that a continuous random real number takes value in a countable set is zero 

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

R4565 
Countable indicator partition of a euclidean real function 

R3200 
Characteristic function of Bernoulli random boolean number 

R1030 
Sigmaalgebra is closed under countable intersections 

R5444 
Expectation of a squared standard gaussian random real number 

R5528 
Determinant zero if a complex square matrix contains two identical rows or two identical columns 

R248 
Binary subadditivity of basic real square root function 

R5471 
Real square matrix invertible iff transpose is 

R4603 


R5358 
Gibbs' inequality for simple relative entropy 

R4390 
Fourier transform characterises euclidean real probability measure 

R4853 
Tight lower bound to simple mutual information 

R4781 
Conditional expectation of known random real number 

R1165 
Reflection invariance of Lebesgue measure 

R292 
Union is smallest upper bound 

R1846 
Cardinality of set complement 

R4112 
Strong fundamental theorem of complex algebra 

R4107 
Determinant of real diagonal matrix with constant diagonal 

R4219 
Dirichlet's theorem 

R4468 
Set of stationary measurable sets is a sigmaalgebra 

R3316 
Pointwise limit of continuous functions need not be continuous 

R5077 
Injection from the natural number plane to the set of natural numbers 

R1034 
Power set is closed under unions 

R4786 
Real conditional covariance partition into conditional moments 

R4073 
Probability of union with the impossible event 

R1194 
Indicator function with respect to set complement 

R5244 
Complex number is zero iff equal to its reflection 

R5558 
Characteristic polynomial for a complex diagonal matrix of constant diagonal 

R2081 
Binary set intersection with empty set is empty 

R1762 
Closed set less open set is closed 

R4616 
The standard mollifier satisfies sufficient conditions required of an approximate identity 

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

R1839 
Cardinality of power set of a finite set 

R2522 
Real conditional expectation given minimal information 

R4322 
Cardinality of finite set union of disjoint sets 

R3414 
Necessary and sufficient condition for convergence of real harmonic series 

R5441 
Variance of a gaussian random real number 

R5439 
Expectation of a chi random unsigned real number 

R4510 
Two complex numbers equal iff difference equals zero 

R4609 


R5519 
Real arithmetic expression for the determinant of a 2by2 real square matrix 

R5125 
Euler's formulas 

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

R5512 
Determinant zero if a real square matrix contains two identical rows or two identical columns 

R3545 
Endpoint bounds for real convex combination 

R4447 


R3367 
Characterisation of convergence of geometric basic real series 

R2623 
Indicator function operator on set of Nsubsets is bijection 

R5620 


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

R4912 
Strong derivative for symmetric euclidean real quadratic form 

R5168 
Infinite product of real numbers in rightclosed unit interval vanishes iff infinite sum of duals diverges 

R1558 
Second fundamental theorem of complex integral calculus 

R4187 
Complement of an Fsigma set is a Gdelta set 

R4832 
Homomorphism property of standard logarithm function in the binary case 

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

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

R262 
Countable union of countable sets is countable 

R4430 
Probability of event in backward orbit under probabilitypreserving endomorphism 

R2079 
Isotonicity of set intersection 

R5093 
Total number of fixedlength sequences using a given number of labels 

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

R4267 
Set intersection with empty set is empty 

R5177 
Young's inequality for two real numbers with standard conjugate exponents 

R5413 


R5297 
Complex conjugate of a product of two complex numbers 

R4901 
Probability density function for standard exponential random positive real number 

R4282 
Standard natural basic real exponential function vanishes at negative infinity 

R3959 
Affine coefficients which minimize expectation of squared distance from a target random real number 

R4783 


R4048 
Number of binary relations on binary cartesian product 

R4597 
Centred gaussian real density function is an even function 

R3038 
Closed graph theorem 

R5324 
Conditional expectation of a random real number conditioned on itself 

R2764 
Canonical singleton map is bijection 

R3184 
Second fundamental theorem of Riemann integral calculus 

R3694 
Lindeberg central limit theorem 

R2964 
Even function equals its even part 

R5292 
Complex conjugate of a complex eigenvalue of a complex matrix is an eigenvalue for the conjugate matrix 

R4560 
Probability of complement of a null event 

R5064 
Cofactor partition for a real square matrix 

R4831 
Homomorphism property of standard logarithm function 

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

R4907 
Strong derivative for constant euclidean real function 

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

R4822 
Conditional probability of the sample space 

R1368 
Jensen's inequality 

R3757 
Linearity of basic real matrix trace 

R979 
Countable subadditivity of measure 

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

R4518 
Equivalent characterisations of finiteness of variance for a random real number 

R4573 
Complex expectation over a null event is zero 

R1166 
Lebesgue measure under scaling 

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

R3931 
Subtracting set from empty set 

R104 
Set of rational numbers is countable 

R4814 
Markov chain triple iff reverse is a Markov chain triple 

R3260 
Weak law of large numbers for random real triangular arrays 

R5073 
Determinant of an upper triangular complex matrix 

R4208 


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

R4132 
Strict version of probabilistic Markov inequality 

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

R4944 
Real binomial theorem for exponent four 

R4689 
Probabilistic Cavalieri principle 

R1371 
Bilinear map is zero if either argument is zero 

R5432 
Expectation of the standard integer random walk after a given number of steps 

R2484 
Moments of a Bernoulli random boolean number 

R4741 
Probabilistic Chebyshov's inequality for square function 

R4705 
Inner product with repeating argument is a real number 

R4943 
Real binomial theorem for exponent three 

R4186 
Complement of a Gdelta set is an Fsigma set 

R5123 


R3472 
Maximum modulus principle 

R301 
Canonical identity map is an injection 

R424 
Euler's identity 

R4961 


R2076 
Inverse image of empty set 

R5518 
Complex arithmetic expression for the determinant of a 2by2 complex square matrix 

R4666 
Real GMHM inequality 

R4158 
Power set is multiplicative 

R2981 
Riemann integral is particular case of Lebesgue integral 

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

R5141 
Real logsumexp method 

R4398 


R4489 
Sigmaalgebra is closed under limit superiors and limit inferiors 

R4074 
Arbitrary intersection of subsets is subset 

R5521 
Signs of length2 standard permutations 

R4280 
Standard natural basic real exponential function is strictly isotone 

R3852 
Transforming random real number to a uniform random real number 

R3640 
Conditional probability given independent sigmaalgebra 

R3746 
Transpose of binary product of real matrices 

R4182 
Isotonicity of sublevel probabilities for a random real number 

R4508 
Two real numbers equal iff difference equals zero 

R4057 
The set of boolean standard sequences is uncountable 

R4161 
Subset of countable intersection iff subset of every set in the intersection 

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

R5486 
Dimension of a euclidean real vector space 

R3897 
Distribution of random finite euclidean real sum is convolution of distribution measures 

R5429 
Maximum likelihood estimator for the common parameter of I.I.D. exponential random positive real numbers 

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

R4469 
Countable union of stationary measurable sets is stationary 

R796 
Principle of weak mathematical induction 

R5567 
Eigenvalue sequence for a diagonal complex matrix with constant diagonal 

R4914 
Derivative for an affine real matrix function 

R4000 
Empty set is clopen 

R2262 
Real variance partition into first and second moments 

R2440 
Translation invariance of Lebesgue outer measure 

R4826 
Logarithm of a ratio 

R3 
Stirling formula 

R2463 
Determinant of a real identity matrix 

R5499 
Dimension of a euclidean complex vector space 

R5076 
Bijection from the natural number plane to the set of natural numbers 

R5555 
Complex arithmetic expression for a complex matrix quadratic form 

R3243 
Constant random variable is independent of any other random variable 

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

R5435 
Expectation of a chisquared random unsigned real number 

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

R1083 
Minimal element is minimum element in ordered set 

R3641 
Conditional probability given independent random variable 

R2871 
Equivalent characterisations of a Schwartz function 

R2113 
Riemann integral of a constant function 

R1824 
Birkhoff ergodic theorem 

R5395 
Factorization need not preserve equality in distribution 

R5334 
Mode maximizes expected number of correct guesses for a finite sequence of discrete random real numbers 

R4315 
Cardinality of a finite set raised to a finite power 

R3911 
Probability density function for standard gaussian random real number 

R3922 
Gaussian random real number is symmetric about its expectation 

R5150 
Global minimizer of subconvex real function iff zero is a subgradient 

R5375 
Riemann integral of decaying standard natural real exponential function over the positive real line 

R3207 
Probability density function for a chisquared random unsigned real number 

R5317 
Intersections need not preserve equality in probabilities for events 

R3602 
Gaussian approximation to binomial distribution 

R4950 
Real matrix with no real eigenvalues 

R5239 
Expectation of standard unsigned uniform random real number 

R4189 


R2599 
Cantor's theorem 

R2395 
Subset of empty set is empty 

R5059 
Adjugate for a 2by2 real square matrix 

R5589 
Eigenvalues of a complex matrix left gramian are unsigned real numbers 

R4537 
Inclusion of inverse image does not imply inclusion of image 

R4164 
Superset of union iff superset of every set in the union 

R4628 
Map to empty set is a surjection 

R828 
First group isomorphism theorem 

R5146 
Standard natural logarithm is superconvex 

R4739 
Binary subadditivity of probability measure 

R2787 
Pascal's rule 

R2182 
Isotonicity of real sublevel sets 

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

R2806 
Standardising a gaussian random real number 

R3600 
Finite sum of independent Poisson random natural numbers is Poisson 

R5505 
Cofactor matrix for a 2by2 real square matrix 

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

R1973 
Map composition is associative 

R5624 
Euclidean real dot product is symmetric 

R2436 
Polar representation of complex conjugate 

R1176 
Inverse image of a constant map is either empty or equal to the domain set 

R354 
Image of singleton set 

R5554 
Real matrix trace is commutation invariant for two real matrices 

R50 
Set difference equals intersection with complement 

R4284 
Standard natural basic real logarithm function escapes to negative infinity at zero 

R4127 
Real exponentiation function with unsigned exponent is isotone on unsigned reals 

R5267 
Probability density function for gaussian random real number 

R5559 
Characteristic polynomial for a complex diagonal matrix 

R2220 
Binary set intersection is commutative 

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

R2658 
Standard natural real logarithm function grows linearly near 1 

R81 
Bilipschitz map is continuous 

R4773 
Inclusionexclusion lower bound to probability of ternary intersection 

R4973 
Biasvariance partition of mean square error for random basic real number 

R4740 


R4157 
Superadditivity of power set 

R466 
Principle of doublenegation is a propositional tautology 

R5192 
CauchySchwarz inequality for two real sequences 

R3941 
Slope function for standard real gaussian density function 

R3535 
Riemann integral of unit semicircle 

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

R4630 
Bijection between parenthesissliced cartesian triple products 

R5523 
Permutation sign sum for complex matrix determinant over the columns 

R2160 
Conditional expectation of known random complex number 

R1848 
Bijection between parenthesissliced cartesian products 

R4095 
Real arithmetic expression for real arithmetic mean 

R5349 
Differential Shannon entropy for an exponential random positive real number 

R4330 
Probability of finite intersection with an almost sure event 

R1242 
Unsigned basic integral is compatible with measure 

R2595 
Convolution identity for binomial coefficient 

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

R1158 
Translation invariance of Euclidean volume function 

R5560 
Characteristic polynomial for a triangular complex matrix 

R4542 
Map is inverse to its inverse 

R5565 
Eigenvalue sequence for a lower triangular complex matrix 

R4733 
Conditional expectation of known random euclidean real number 

R1567 
Positive real geometric mean expressed in terms of real arithmetic mean 

R5194 


R4686 
Probabilistic Chebyshov's inequality for an exponentiation function 

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

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

R5466 
Linear slope which minimizes expectation of squared distance from a target random real number 

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

R4668 
Transpose of a finite product of complex matrices 

R293 
Open set less closed set is open 

R5430 
Growth rate for the expectation of the absolute value of the standard integer random walk 

R755 
Group centre is Abelian group 

R4697 
Simple integral of a measurable simple function with respect to a point measure 

R2746 
Finite sets are closed in Fréchet space 

R5304 
Complexlinearity of real expectation 

R1073 
Mean value theorem 

R2254 
Riemann integral of standard real gaussian function 

R2928 
Finite sum of even euclidean real functions is even 

R3744 
Real arithmetic expression for a real matrix quadratic form 

R4294 
Set difference with finite minuend is finite 

R3532 
Tautological pointwise lower bound from indicator function on sublevel set 

R4160 
Subset of intersection iff subset of every set in the intersection 

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

R756 
Abelian group iff centre is whole group 

R4906 


R4321 
Set and set complement are disjoint 

R5530 
Determinant of a scaled real matrix 

R4339 
Conditional probability of almost surely false event 

R5219 
Meanvalue theorem applied to the standard unit semicircle function 

R2071 
Isotonicity of set union 

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

R5627 
Complex matrix multiplied by a complex column matrix from the right 

R4461 


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

R5643 
Cardinality of the set of bytes 

R3938 
Upper and lower bounds for codomain set of probability measure 

R5404 
I.I.D. real central limit theorem 

R4038 
Product of two finite real sums 

R976 
Finite disjoint additivity of unsigned basic measure 

R3061 
Real Riemann integral over a reflected interval 

R244 
Convergent sequence is Cauchy 

R3749 
Partition of real square matrix into sum of symmetric and antisymmetric parts 

R2548 
Constant map pulls back a bottom sigmaalgebra 

R4378 
Independent random basic real pair iff distribution functions factorise 

R5557 
Complex matrix characteristic polynomial is a monic polynomial with degree equal to row and column dimensions 

R4905 
Derivative for standard natural real logarithm function 

R3461 
Holomorphic function with vanishing derivative on complex domain is constant 

R2959 
Function even part is even 

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

R2782 
Arithmetic expression for sum of initial natural numbers 

R352 
Inverse image of image 

R2812 
Finite variance implies finite expectation for random real number 

R4281 
Standard natural basic real exponential function is escapes to positive infinity at positive infinity 

R4341 
Bayes' theorem in the case of two pullback events 

R4291 
Vector space always has an inclusionmaximal linearly independent set 

R4617 
The standard mollifier integrates to one 

R1120 
Antitonicity of minimum 

R4207 


R2933 
Isotonicity of countably infinite real summation 

R4055 
Singleton map is injection from set to power set 

R4691 
Expectation of random natural number by summing tail probabilities 

R4568 
Countable indicator partition of a random complex number 

R2112 
Isotonicity of Riemann integral 

R5535 
Reciprocals form an eigenvalue sequence for complex matrix inverse 

R3995 
Complex binomial theorem 

R4795 
Real calculus expression for distribution function of exponential random positive real number 

R2055 
Cavalieri principle for basic real Riemann integral calculus 

R984 
Transforming an isotone sequence of sets into pairwise disjoint sequence with common limit 

R3618 
Turning two unsigned real numbers into convex combination coefficients 

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

R4563 
Complex integral over a set of measure zero is zero 

R2310 
Distribution formula for unsigned basic integral 

R5490 
Real matrix injective iff kernel trivial 

R5144 
Vanishing gradient identifies a minimizer for differentiable subconvex real function 

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

R738 
Left and right cosets coincide in Abelian group 

R2075 
Image of empty set 

R507 
Empty set is countable 

R5226 
Tight lower bound on the probability for two independent Bernoulli random boolean numbers to coincide 

R4970 


R2934 
Isotonicity of unsigned basic real series 

R2339 
Finite sum of uncorrelated gaussian random real numbers is a gaussian random real number 

R75 
Intersection of closed sets is closed 

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

R5568 
Eigenvalue sequence for an identity complex matrix 

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

R5327 
Expectation of a standard exponential random positive real number 

R5569 
Determinant of reflected complex matrix 

R2413 
Complex conjugate of real number 

R3883 
Rowstandardisation of rowindependent random real triangular array 

R1401 
Orthogonality relation is a symmetric binary relation 

R4765 
Reflection preserves euclidean real subset relation 

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

R2374 
BorelCantelli zeroone law 

R2368 
I.I.D. real strong law of large numbers with the identity index sequence 

R5365 
A singleton real set is standard Borel 

R1831 
Real arithmetic expression for binomial coefficient 

R4001 
Whole space is clopen 

R511 
Natural number plane is countable 

R5361 
A countable real set is standard Borel 

R3503 
Data processing inequality 

R4278 
Expression for probability of event in terms of complement event 

R5061 
Expression for a real matrix inverse in terms of adjugate 

R4787 


R4222 
Quotienting a set reduces its cardinality 

R5619 


R5336 
Expectation of an indicator random boolean number 

R4216 
Finite set intersection is invariant under bijective shifting of indices 

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

R4927 
Binary partition additivity of unsigned basic measure 

R1177 
Constant map is always measurable 

R5069 
Determinant of a diagonal complex matrix 

R3874 


R3617 
Turning a finite number of unsigned real numbers into convex combination coefficients 

R5368 
Uniform distribution is the maximum simple Shannon entropy distribution for fixed alphabet 

R4665 
Weighted real GMHM inequality 

R4334 
Every nonempty finite graph contains a bipartite subgraph with at least half the edges 

R4841 
Finite disjoint additivity of probability measure 

R3621 
Standard natural exponential function equals powers of Napier's constant 

R1575 
Goursat's theorem for rectangles 

R347 
Isotonicity of map image 

R4288 


R465 
De Morgan's laws are propositional tautologies 

R4855 
Reflection property of standard logarithm function 

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

R4989 
Information inequality for simple relative entropy 

R74 
Finite union of closed sets is closed 

R5536 
Eigenvalues of a conjugate symmetric complex matrix are real 

R4599 
Density partition for expectation of a random real number 

R4685 
I.I.D. weak law of large numbers for random real numbers of finite first absolute moments 

R5300 
Unsigned basic integral over an empty set equals zero 

R5423 
Wald's second equation under independence 

R1338 
Probabilistic BorelCantelli lemma 

R4846 
Conditional simple entropy with respect to itself 

R1370 
Multilinear map is zero if any argument is zero 

R4706 
Complex conjugate zero iff argument zero 

R5169 
Infinite product of real numbers in rightclosed unit interval does not vanish iff infinite sum of duals converges 

R5527 
Interchanging two rows or two columns of a complex square matrix switches the sign of the determinant 

R80 
Lipschitz map is continuous 

R87 
Convolution is commutative 

R5544 
Real matrix trace is preserved by transposing 

R4372 
Independent random real pair is uncorrelated 

R1557 
Weighted real AMGM inequality 

R4678 
Independent finite random real collection is uncorrelated 

R1369 
Jensen's inequality for expectation 

R4594 
Real calculus expression for central moments of gaussian random real number about expectation 

R4886 
Characterisation of a quotient set by proper set partitions 