
R1846 
Cardinality of set complement 

R2220 
Binary set intersection is commutative 

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

R4174 
Proper contraction has at most a single fixed point 

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

R1193 
Finite product of indicator functions equals indicator of intersection 

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

R3461 
Holomorphic function with vanishing derivative on complex domain is constant 

R3503 
Data processing inequality 

R4919 
Measurable transformation preserves independent countable random collection 

R1558 
Second fundamental theorem of complex integral calculus 

R1077 
Maximum element is unique 

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

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

R4290 
Vector space always has a linearly independent subset 

R347 
Isotonicity of map image 

R4508 
Two basic real numbers equal iff difference equals zero 

R2522 
Basic real conditional expectation given minimal information 

R4794 
Independent minimums preserve exponential distribution 

R4904 
Strong derivative for basic real square function 

R4848 
Probability of event conditional on complement 

R112 
Cavalieri principle 

R2833 
Nonempty set is singleton iff all elements equal each other 

R3869 
Rowstandardisation of rowindependent random basic real standard triangular array 

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

R2914 
CantorBernstein theorem 

R2960 
Function odd part is odd 

R4269 
Countable set union with empty set 

R4518 
Equivalent characterisations of finiteness of basic real variance 

R2081 
Binary set intersection with empty set is empty 

R322 
Image of projection map 

R4038 
Binary product of finite basic real sums 

R4370 
Set of euclidean natural numbers has Lebesgue measure zero 

R3983 
Subcollection of independent collection of sigmaalgebras is independent 

R3494 
GlivenkoCantelli theorem 

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

R80 
Lipschitz map is continuous 

R3923 
Standard gaussian random basic real number is symmetric about zero 

R1064 
Isotonicity of Lebesgue measure 

R2719 
Affine majorant for the standard natural logarithm 

R4846 
Conditional simple entropy with respect to itself 

R4991 
Complex matrix multiplied from the right by a diagonal matrix 

R1832 
Cardinality of a finite cartesian product of finite sets 

R4899 


R4805 
Dual probability distribution function for geometric random basic positive integer 

R4168 
Difference of set and countable intersection equals union of differences 

R5074 
Determinant of a lower triangular complex matrix 

R5049 


R3757 
Linearity of basic real matrix trace 

R4438 
Equivalent characterisations of ergodicity for probabilitypreserving system 

R4049 
Number of binary relations on a finite set 

R4889 
Basic random variable almost surely finite if expectation finite 

R3589 
Random basic number almost surely finite if expectation is finite 

R3200 
Characteristic function of Bernoulli random boolean number 

R4765 
Reflection preserves euclidean real subset relation 

R3919 
Probability measure need not be an injection 

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

R4903 
Strong derivative for affine basic real function 

R2016 
Probabilistic Markov's inequality 

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

R4591 
Binary additivity of transpose for basic real matrices 

R371 
Countable set iff injection to natural numbers 

R233 
Whole space is closed 

R3958 
Intersecting subtrahend with minuend preserves set difference 

R4398 


R2767 
Identity map is an injection 

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

R4961 


R4303 
Nonempty finite poset contains a maximal element 

R3695 
Standardised Lindeberg central limit theorem 

R4470 
Inverse image of countable union is union of inverse images 

R468 
Lagrange's theorem 

R4755 
Inverse image of reflected basic real set 

R4699 


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

R4902 
Strong derivative for constant basic real function 

R2413 
Complex conjugate of real number 

R4667 
Basic real function which is strongly differentiable only at a single point 

R4702 


R708 
Reverse triangle inequality for metric 

R4692 


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

R4780 
Basic real conditional expectation given independent sigmaalgebra 

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

R4788 


R976 
Finite disjoint additivity of unsigned basic measure 

R5066 
Inverse of symmetric complex matrix is symmetric 

R4444 
Superset differenced from set equals empty set 

R1960 
Characterisation of measurepreserving transformations by signed integral 

R3515 
Unsigned basic integral zero iff function almost everywhere zero 

R4992 
Complex matrix multiplied from the left by a diagonal matrix 

R4773 
Inclusionexclusion lower bound to probability of ternary intersection 

R1089 
Characterisation of convergent sequences in metric space 

R4606 


R3204 
Characteristic function of geometric random positive integer 

R310 
Rightinvertible map iff surjection 

R4213 
Countable set union is invariant under bijective shifting of indices 

R2754 
Lipschitz map is Hölder continuous 

R2093 
Countable subadditivity of probability measure 

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

R2782 
Sum of initial natural numbers 

R3304 
Approximating sequence for the natural exponential function 

R4464 


R3984 
Subcollection of independent random collection is independent 

R3860 
Quantile function is inverse to invertible distribution function for random basic real number 

R2079 
Isotonicity of set intersection 

R2981 
Riemann integral is particular case of Lebesgue integral 

R2966 
Indicator function under scaling of the argument 

R88 
Convolution is associative 

R2641 
Euclidean real martingale is constant in expectation 

R4293 
Power set of a finite set is finite 

R4950 
Real matrix with no real eigenvalues 

R4275 
Absolute value function is an even basic real function 

R3532 
Tautological pointwise lower bound from indicator function on sublevel set 

R4093 
Basic real harmonic and arithmetic means are multiplicative inverses when arguments are 

R3911 
Probability density function for standard gaussian random basic real number 

R49 
Isotonicity of subtracting same set 

R3183 
First fundamental theorem of Riemann integral calculus 

R4467 
Empty set is a stationary measurable set 

R1160 
Reflection invariance of Euclidean volume function 

R1540 
Affine map preserves convex sets in images 

R3507 
Binary union of countable sets is countable 

R2343 
Uncorrelated basic real weak law of large numbers 

R714 
Element belongs to its own equivalence class 

R4776 
Hoeffding's lemma 

R4278 
Expression for probability of event in terms of complement event 

R2370 
Basic real arithmetic expression for cardinality of countable set 

R5072 
Determinant of triangular complex matrix 

R3652 
CramérWold theorem 

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

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

R4801 
Probability mass function for cogeometric random basic natural number 

R4274 
Absolute value function escapes to positive infinity in both directions 

R4996 


R1034 
Power set is closed under unions 

R2929 
Sum of odd functions is odd 

R1530 
Inverse image preserves set difference 

R2092 
Sequential continuity of probability measure from above 

R4330 
Probability of finite intersection with an almost sure event 

R4011 
Polish space is secondcountable 

R797 
Principle of weak mathematical induction on the natural numbers 

R3942 
Derivative of gaussian basic real density function 

R354 
Image of singleton set 

R4349 
Two disjoint events independent iff one is of probability zero 

R2764 
Canonical singleton map is bijection 

R4748 


R2373 
Second probabilistic BorelCantelli lemma 

R2788 
Real binomial theorem 

R50 
Set difference equals intersection with complement 

R4895 
Standard counting measure is a pointmass measure 

R25 
CauchySchwarz inequality 

R237 
Intersection distributes over union 

R2780 
Upper bound for number of arrows in finite digraph 

R2783 
Sum of initial natural numbers squared 

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

R4580 
Empty set union equals the empty set 

R3543 
Endpoint bounds for basic real affine combination 

R4264 
Cartesian product with empty set is empty 

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

R4834 


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

R2310 
Distribution formula for unsigned basic integral 

R2112 
Isotonicity of Riemann integral 

R3412 
Euclidean real arithmetic mean minimises Euclidean distance 

R4932 


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

R4817 
Data processing inequality for transformed endpoint 

R3646 
Countable partition additivity of probability measure 

R5068 
Determinant of scaled complex matrix 

R2368 
I.I.D. strong law of large numbers for random real numbers 

R4207 


R4463 
Strongly mixing probabilitypreserving system is weakly mixing 

R3922 
Gaussian random basic real number is symmetric about its expectation 

R4871 
Translation property of the standard logsumexp function 

R4774 


R3694 
Lindeberg central limit theorem 

R4855 
Reflection property of standard logarithm function 

R4804 
Probability distribution function for geometric random basic positive integer 

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

R4308 
Map composition need not be commutative 

R1242 
Unsigned basic integral is compatible with measure 

R3904 
Characteristic function of a Poisson random natural number 

R2067 
Subtracting empty set from set 

R4583 


R4639 
Characteristic function of translated random basic real number 

R2537 
Basic real exponentiation function with positive exponent is strictly isotone on positive basic reals 

R1851 
Cardinality of set of permutations on finite set 

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

R4905 
Strong derivative for standard natural basic real logarithm function 

R4483 
Basic real number is zero iff equal to its reflection 

R4295 
Power set of a countable set need not be countable 

R4982 
Exchangeable random collection is identically distributed 

R1074 
Rolle's theorem 

R4831 
Homomorphism property of standard logarithm function 

R4329 
Probability of countable intersection with an almost sure event 

R4769 


R4559 
Probability of complement of an almost sure event 

R4733 
Conditional expectation of known random euclidean real number 

R2182 
Isotonicity of basic real sublevel sets 

R4431 


R4698 
Unsigned basic integral with respect to a point measure 

R4906 


R2441 
Reflection invariance of Lebesgue outer measure 

R4732 


R1070 
Extreme value theorem for basic real calculus 

R3383 
Stein's lemma 

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

R4152 


R2687 
Approximating function for the natural exponential function 

R4541 
Open set is its own interior 

R220 
Difference of set and union equals intersection of differences 

R3863 
Signed basic integral with respect to a point measure 

R3529 
Tautological pointwise inequality from indicator functions on sublevel sets 

R4331 
Probability of binary intersection with an almost sure event 

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

R1177 
Constant map is always measurable 

R4825 
Bit entropy of a standard bernoulli number is one bit 

R3852 
Transforming random basic real number to uniform random basic real number 

R1575 
Goursat's theorem for rectangles 

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

R4287 
Finite product of even complex functions is even 

R1818 
Isotonicity of basic real expectation 

R2876 
Basic mean value inequality 

R4538 
Inclusion of image does not imply inclusion of inverse image 

R2091 
Sequential continuity of probability measure from below 

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

R463 
Law of the excluded middle is a propositional tautology 

R2741 
Set equality iff inclusion in both directions 

R2599 
Cantor's theorem 

R4853 
Tight lower bound to simple mutual information 

R2464 
Determinant is preserved under transpose of complex matrix 

R5009 
Bernoulli random boolean integer from a uniform random basic real number 

R447 
Zorn's lemma 

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

R2436 
Polar representation of complex conjugate 

R4767 


R3205 
Probability mass function for geometric random positive integer 

R755 
Group centre is Abelian group 

R4267 
Set intersection with empty set is empty 

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

R3778 
Probability density function for exponential random positive basic real number 

R4272 
Absolute value function is not strictly antitone 

R4676 


R4140 
Standardised Mill's inequalities 

R590 
Square root of two is irrational 

R975 
Isotonicity of unsigned basic measure 

R2658 
Asymptotic results for standard logarithm function 

R4368 
Set of euclidean integers has Lebesgue measure zero 

R3642 
Law of total probability for complement partition 

R5069 
Determinant of diagonal complex matrix 

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

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

R2262 
Basic real variance partition into first and second moments 

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

R3517 
Unsigned basic expectation zero iff random number almost surely zero 

R3595 
Probabilistic Tonelli's theorem 

R4703 


R1904 
Isotonicity of finite basic real summation 

R2367 
Law of total variance 

R2100 
Triangle inequality for signed basic expectation 

R4573 
Complex expectation over a null event is zero 

R5097 
Power set is isomorphic to a set of boolean functions 

R3974 
Sum of independedent standard chisquard random basic real numbers is chisquared 

R4598 
Standard gaussian basic real density function is an even function 

R4630 
Bijection between parenthesissliced cartesian triple products 

R5086 
Eigenvectors of a symmetric real matrix are orthogonal 

R4286 
Standard natural basic real logarithm function maps one to zero 

R3582 
Signed expectation finite iff absolutely integrable random basic number 

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

R4823 
Conditional probability of the empty event 

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

R3640 
Conditional probability given independent sigmaalgebra 

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

R3544 
Endpoint bounds for basic real arithmetic mean 

R4970 


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

R4486 
Metric space is Hausdorff 

R508 
Finite cartesian product of countable sets is countable 

R796 
Principle of weak mathematical induction 

R3605 
Subadditivity of basic real square root function 

R1204 
Fatou's lemma for unsigned basic integral 

R4009 
Metrisable topological space is Fréchet 

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

R301 
Canonical identity map is an injection 

R4348 
Two disjoint events are not necessarily independent 

R4087 
Real arithmetic expressions for OR boolean logic gate 

R4261 
Basic real binomial theorem for exponent two 

R3262 
Dilations of unsigned tail probability converge to zero 

R4674 


R2062 
Antitonicity of subtracting from the same set 

R3912 
Characteristic function of rademacher random basic integer 

R5099 
Sum of initial natural numbers cubed 

R2411 
Characteristic function of exponential random basic real number 

R2656 
De MoivreLaplace theorem 

R4912 
Strong derivative for symmetric euclidean real quadratic form 

R4390 
Fourier transform characterises euclidean real probability measure 

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

R2440 
Translation invariance of Lebesgue outer measure 

R3038 
Closed graph theorem 

R1487 
Ring is a subring of itself 

R246 
Cauchy sequence is bounded 

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

R4808 
Affine transformations preserve independent basic real pairs 

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

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

R4851 
Tight upper bound to simple entropy 

R4372 
Independent random basic real pair is uncorrelated 

R4943 
Basic real binomial theorem for exponent three 

R270 
Basic real arithmetic expression for sum of finite basic real geometric sequence 

R4898 


R4520 
Complex conditional expectation is absolutely integrable 

R4847 
Probability of event conditional on itself 

R5075 
Complex matrix determinant is multiplicative 

R3908 
Characteristic function of almost surely constant random euclidean real number 

R3896 
Expectation is idempotent 

R4720 
Conditional probability of complement event 

R293 
Open set less closed set is open 

R4455 


R3747 
Transpose of finite product of finite basic real matrices 

R2506 
Independent random real collection is uncorrelated 

R4701 


R4339 
Conditional probability of almost surely false event 

R4187 
Complement of an Fsigma set is a Gdelta set 

R1975 
Measure of set in backward orbit under measurepreserving endomorphism 

R4688 
Second moment upper bound to basic real variance 

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

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

R4189 


R1903 
Basic integral of almost everywhere zero function is zero 

R2407 
Measurable transformation preserves independence 

R2928 
Finite sum of even euclidean real functions is even 

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

R4686 
Probabilistic Chebyshov's inequality for an exponentiation function 

R1076 
Minimum element is unique 

R4350 
Finite superadditivity of finite set cardinality 

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

R4456 


R2747 
Finite sets are closed in Hausdorff space 

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

R3179 
Basic real binomial inequality 

R2270 
Sigmaalgebra is closed under symmetric differences 

R4739 
Binary subadditivity of probability measure 

R4327 
Probability of countable union with an almost sure event 

R4369 
Set of euclidean rational numbers has Lebesgue measure zero 

R2989 
Unsigned basic Lebesgue integral under scaling 

R4814 
Markov chain triple iff reverse is a Markov chain triple 

R4273 
Absolute value function preserves zero 

R4383 
Euclidean real Fourier transform is uniformly bounded 

R248 
Binary subadditivity of basic real square root function 

R2959 
Function even part is even 

R1370 
Multilinear map is zero if any argument is zero 

R2483 
Variance of Bernoulli random boolean number 

R4563 
Complex integral over a set of measure zero is zero 

R4596 
Basic real calculus expression for moments of standard gaussian random basic real number 

R2588 
Weak Stirling formula 

R977 
Ambient set is union of subset and complement of subset 

R4265 
Finite set intersection with empty set is empty 

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

R3198 
Finite sum of uncorrelated Poisson random natural numbers is Poisson 

R3513 
Measurable subnull set has measure zero 

R4843 
Conditional entropy formula for simple mutual information 

R3498 
Homomorphism property of the standard natural logarithm 

R4915 


R800 
Proof by principle of weak mathematical induction 

R2732 
Kolmogorov zeroone law 

R1213 
Linearity of unsigned basic integral 

R4838 
Sum rule for simple marginal probability 

R4473 
Almost idempotency of conditional expectation of random complex number 

R2690 
Minimum and maximum of stopping times are stopping times 

R3749 
Decomposition of basic real square matrix into sum of symmetric and antisymmetric parts 

R1234 
BorelCantelli lemma 

R2615 
Empty set is cofinite within a finite set 

R1839 
Cardinality of power set of a finite set 

R1164 
Translation invariance of Lebesgue measure 

R4280 
Standard natural basic real exponential function is strictly isotone 

R4048 
Number of binary relations on binary cartesian product 

R4183 
Alternative basic real arithmetic expressions for Catalan sequence 

R4770 
Inclusionexclusion lower bound to probability of binary intersection 

R4169 
Difference of set and finite intersection equals union of differences 

R3601 
Gaussian approximation to standard Poisson distribution 

R1603 
De Moivre's theorem 

R4729 
Complex binomial inequality 

R4627 


R3748 
Finite basic real matrix is positive definite iff symmetric part is 

R457 
Fréchet space iff singletons are closed 

R4012 
Polish space is Hausdorff 

R244 
Convergent sequence is Cauchy 

R893 
Cyclic group is Abelian 

R2751 
Fourier transform of absolutely integrable function is bounded 

R4741 
Probabilistic Chebyshov's inequality for square function 

R648 
Proportionally bounded linear map is Lipschitz 

R4171 
Difference of set and countable union equals intersection of differences 

R4127 
Basic real exponentiation function with unsigned exponent is isotone on unsigned basic reals 

R3745 
Basic real square matrix antisymmetric part is zero definite 

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

R4737 


R3514 
Unsigned basic expectation over set of probability zero is zero 

R4304 
Nonempty finite poset contains a minimal element 

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

R4276 
Triangle inequality for absolute value function 

R4925 
Probability calculus expression for conditional probability given disjoint nonnull partition 

R3472 
Maximum modulus principle 

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

R4159 
Power set is not empty 

R2589 
Trivial factorial upper bound 

R1824 
Birkhoff ergodic theorem 

R4321 
Set and set complement are disjoint 

R3231 
Riemann integral analogue to infinite geometric series 

R10 
Binary cartesian product with empty set is empty 

R4704 


R4500 


R4916 


R4260 
Basic real square root function is strictly isotone 

R4693 


R1959 
Young's inequality 

R1178 
Continuous map is Borel measurable 

R3649 
Expectation of conditional probability 

R2746 
Finite sets are closed in Fréchet space 

R4626 
Strict isotonicity of basic Riemann integral 

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

R1012 
Monotonicity of real limits 

R2219 
Set intersection is associative 

R47 
Set difference is subset of the minuend 

R1401 
Orthogonality relation is a symmetric binary relation 

R5073 
Determinant of an upper triangular complex matrix 

R1232 
Tonelli's theorem for sums and integrals 

R4288 


R3680 
Characteristic function of standard gaussian random real number 

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

R292 
Union is smallest upper bound 

R4909 
Strong derivative for selfdot product function 

R3770 
Product of finite basic real 2by2 matrix with its transpose 

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

R4089 
Real arithmetic expressions for NAND boolean logic gate 

R4338 
Conditional probability of almost surely true event 

R1236 
Markov's inequality 

R4568 
Countable indicator partition of a random complex number 

R2141 
Reflection invariance of unsigned basic Lebesgue integral 

R4118 
Basic real arithmetic expression for unsigned basic real geometric mean 

R2259 
Variance of a finite sum of random basic real numbers 

R5080 
Complex matrix determinant nonzero iff kernel is trivial 

R4540 
Inverse map is a bijection 

R4787 


R4340 
Bayes' theorem in the case of event and complement 

R3385 
Standard approximating sequence for the natural exponential function 

R4447 


R4800 
Number of injections from a finite set to itself 

R4132 
Strict version of probabilistic Markov inequality 

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

R2897 
Fourier transform under scaling 

R4013 
Polish space is Fréchet 

R4215 
Countable set intersection is invariant under bijective shifting of indices 

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

R75 
Intersection of closed sets is closed 

R3518 
Partition of random basic number into positive and negative parts 

R108 
Inclusion iff reverse inclusion of complements 

R4609 


R2748 
Finite sets are closed in metric space 

R1406 
Collection of sets ordered by inclusion contains a maximal element 

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

R2082 
Binary set union with empty set 

R2437 
Euclidean real Fourier inversion theorem 

R1869 
Characterisation of equality of maps 

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

R3542 
Jensen's inequality for finite basic real arithmetic mean 

R1170 
Euclidean volume of singleton 

R4668 
Transpose of finite product of finite complex matrices 

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

R1856 
Cardinality of the set of maps between finite sets 

R81 
Bilipschitz map is continuous 

R507 
Empty set is countable 

R4689 
Probabilistic Cavalieri principle 

R5085 
Eigenvalues of a symmetric real matrix are realvalued 

R2938 
Vanishing sequence is necessary for finiteness of real series 

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

R2525 
Independence of sigmaalgebras is hereditary 

R3429 
Complex conjugation is multiplicative operation 

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

R4469 
Countable union of stationary measurable sets is stationary 

R2986 
Lebesgue outer measure under scaling 

R4001 
Whole space is clopen 

R3508 
Fermat's last theorem 

R979 
Countable subadditivity of measure 

R4706 
Complex conjugate zero iff argument zero 

R4282 
Standard natural basic real exponential function vanishes at negative infinity 

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

R4901 
Probability density function for standard exponential random positive basic real number 

R2086 
Finite inclusionexclusion principle for unsigned basic measure 

R4738 
Finite subadditivity of probability measure 

R3020 
Complex Lebesgue integral under scaling 

R822 
Group of prime order is cyclic 

R1073 
Mean value theorem 

R2313 
Expectation with dual probability distribution function 

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

R1854 
Cardinality of the set of injections between finite sets 

R4341 
Bayes' theorem in the case of two pullback events 

R1214 
Isotonicity of unsigned basic integral 

R4610 


R3260 
Weak law of large numbers for random real triangular arrays 

R3506 
Finite union of countable sets is countable 

R4277 
Measure of measurable set complement 

R1237 
Unsigned basic Borel function almost everywhere finite if integral is finite 

R4757 
Young's inequality for two basic real numbers 

R3746 
Transpose of binary product of finite basic real matrices 

R4695 
Infinite product of basic real numbers on the open unit interval need not converge to zero 

R4333 
Binary product of indicator functions equals indicator of intersection 

R4170 
Difference of set and binary intersection equals union of differences 

R1171 
Isotonicity of Euclidean volume function 

R2786 
Complement property of binomial coefficient 

R1130 
Intersection is largest lower bound 

R1131 
Image of inverse image 

R4443 
Measure of symmetric difference of set and subset 

R4921 
Affine transformations preserve independent countable basic real collection 

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

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

R4445 
Inclusionexclusion principle for probability of binary union 

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

R5092 
Probability of binary intersection with a null event 

R4947 
Variance of standard Bernoulli random boolean number 

R4537 
Inclusion of inverse image does not imply inclusion of image 

R24 
Parallelogram identity 

R2744 
Square root of prime is irrational 

R1841 
Indicator function operator is a bijection 

R4795 
Basic real calculus expression for exponential distribution function 

R4073 
Probability of union with impossible event 

R4944 
Basic real binomial theorem for exponent four 

R4811 
Markov chain triple iff endpoints conditionally independent 

R1450 
Explicit algebraic expression for elements of generated subgroup 

R3935 
Superset iff equal to union with subset 

R4182 
Isotonicity of sublevel probabilities for random basic real number 

R4466 
Whole space is a stationary measurable set 

R4086 
Real arithmetic expressions for AND boolean logic gate 

R1202 
Dominated convergence theorem for signed basic integral 

R3504 
Erdős discrepancy problem 

R4948 
Gaussian approximation to standard binomial distribution 

R2871 
Equivalent characterisations of a Schwartz function 

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

R4809 
Affine transformations preserve independent finite basic real collection 

R3545 
Endpoint bounds for basic real convex combination 

R3404 
Bayes' theorem in the case of two events 

R1165 
Reflection invariance of Lebesgue measure 

R2089 
Unsigned basic expectation is compatible with probability measure 

R4511 
Two complex numbers distinct iff difference distinct from zero 

R2090 
Isotonicity of probability measure 

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

R4597 
Centred gaussian basic real density function is an even function 

R2964 
Even function equals its even part 

R1488 
Group is a subgroup of itself 

R3479 
Conformal complex function iff holomorphic bijection 

R4292 
Finite cartesian product of finite sets is finite 

R3641 
Conditional probability given independent random variable 

R3207 
Probability density function for a chisquared random unsigned basic real number 

R2224 
Set union is associative 

R2076 
Inverse image of empty set 

R2075 
Image of empty set 

R1369 
Jensen's inequality for expectation 

R2963 
Odd function equals its odd part 

R4836 
Change of base formula for simple entropy 

R1906 
Isotonicity of limits of basic real sequences 

R4607 
Pushforward change of variables formula for unsigned basic integral 

R4536 
Map image empty iff underlying set empty 

R4679 
Independent countable random basic real collection is uncorrelated 

R4914 
Derivative for affine real matrix function 

R3954 
Two almost surely equal random variables are identically distributed 

R4172 
Difference of set and finite union equals intersection of differences 

R431 
Set of integers is countable 

R5091 
Lindeberg central limit theorem for a standard triangular array 

R4214 
Finite set union is invariant under bijective shifting of indices 

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

R3568 
Basic real arithmeticgeometric mean inequality 

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

R3416 
Absolute value bounds for a basic real number 

R4328 
Probability of finite union with an almost sure event 

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

R1158 
Translation invariance of Euclidean volume function 

R4876 


R4727 
Euclidean real binomial inequality 

R4637 


R978 
Measure of set difference 

R2740 
Splitting a Riemann integral over an implicit interval partition 

R370 
Countable set iff surjection from natural numbers 

R982 
Sequential continuity of measure from below 

R3215 
Characteristic function of indicator random boolean number 

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

R4971 


R1557 
Basic real multiplicativeadditive convex combination inequality 

R4294 
Set difference with finite minuend is finite 

R125 
Subset relation is reflexive 

R1902 
Signed basic integral of almost everywhere equal functions 

R4781 
Conditional expectation of known random basic real number 

R1022 
Partition of basic function into positive and negative parts 

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

R262 
Countable union of countable sets is countable 

R2160 
Conditional expectation of known random complex number 

R4728 


R4560 
Probability of complement of a null event 

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

R3612 
Standard natural basic real logarithm function is strictly isotone 

R4926 
Finite partition additivity of unsigned basic measure 

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

R4000 
Empty set is clopen 

R4740 


R4090 
Real arithmetic expressions for XOR boolean logic gate 

R4158 
Power set is multiplicative 

R4566 
Countable indicator partition of a complex function 

R2405 
Characteristic function identifies distribution of random basic real number 

R4888 
Isotonicity of set cardinality 

R4764 


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

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

R4599 
Density partition for expectation of random basic real number 

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

R4157 
Superadditivity of power set 

R2623 
Indicator function operator on set of Nsubsets is bijection 

R1159 
Euclidean volume function under scaling 

R4314 
Number of boolean functions on a finite set 

R1075 
Basic real interior extremum theorem 

R4291 
Vector space always has an inclusionmaximal linearly independent set 

R4430 
Probability of event in backward orbit under probabilitypreserving endomorphism 

R1838 
Cardinality of finite set union of finite sets 

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

R4743 
Riemann integral average of vanishing unsigned basic real function vanishes 

R2485 
Expectation of geometric random basic positive integer 

R4920 
Measurable transformation preserves independent finite random collection 

R4997 


R2164 
Law of the excluded middle in probability calculus 

R4907 
Strong derivative for constant euclidean real function 

R465 
De Morgan's laws are propositional tautologies 

R4387 
Characteristic function of standard Poisson random natural number 

R4666 
Basic real geometricharmonic mean inequality 

R4509 
Two basic real numbers distinct iff difference distinct from zero 

R87 
Convolution is commutative 

R4543 
Map inverse is invertible 

R2806 
Standardising a gaussian random real number 

R4141 
Probabilistic Chernoff inequality 

R4485 
Convergent sequence in metric space has unique limit point 

R4665 
Basic real weighted GMHM inequality 

R4010 
Polish space is firstcountable 

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

R1577 
Cauchy's theorem for a disc 

R4782 
Expectation of basic real conditional expectation 

R1035 
Power set is closed under intersections 

R315 
Composition of surjections is surjection 

R4945 
Basic real binomial theorem for exponent five 

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

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

R4060 
Appropriately parenthesised cartesian products are isomorphic 

R4611 


R4128 
Two random real numbers identical in distribution have identical moments 

R4826 
Logarithm of a ratio 

R2377 
Almost sure convergence implies convergence in probability 

R4453 
Probability of symmetric difference of event and subevent 

R4747 


R102 
Singletons are closed in a metric space 

R4621 
Standard mollifier is an approximate identity for complex Lebesgue convolution 

R464 
Ex falso sequitur quodlibet 

R3367 
Characterisation of convergence of geometric basic real series 

R1973 
Map composition is associative 

R2221 
Set intersection is invariant under bijective shifting of indices 

R3401 
Probability calculus expression for conditional expectation given disjoint nonnull partition 

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

R2934 
Isotonicity of unsigned basic real series 

R1275 
Every map to trivial topological space is continuous 

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

R4869 
Characterisation of superconvex basic real functions 

R432 
Set of natural numbers is countable 

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

R4173 
Difference of set and binary union equals intersection of differences 

R1368 
Jensen's inequality 

R4317 
Inclusionexclusion principle for unsigned basic measure of ternary union 

R4092 
Basic real arithmetic expression for basic real harmonic mean 

R4332 


R2484 
Moments of Bernoulli random boolean number 

R1120 
Antitonicity of minimum 

R7 
Empty set is subset of every set 

R4662 
Signed basic expectation with respect to a point probability measure 

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

R4315 
Cardinality of a finite set raised to a finite power 

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

R1166 
Lebesgue measure under scaling 

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

R1868 
Composition of indicator function with set endomorphism 

R3201 
Characteristic function of a binomial random natural number 

R2505 
Basic real covariance partition into first moments 

R511 
Natural number plane is countable 

R4886 
Characterisation of a quotient set by proper set partitions 

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

R3 
Stirling formula 

R4669 
Diagonalizable complex matrix is symmetric 

R981 
Countably infinite measurable cover has measurable subcover 

R4289 
Vector space always has a basis 

R4827 
Entropy of a standard bernoulli number 

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

R4510 
Two complex numbers equal iff difference equals zero 

R2222 
Set union is invariant under bijective shifting of indices 

R831 
Second group isomorphism theorem 

R4930 


R5059 
Adjugate for 2by2 real matrix 

R255 
Power set of empty set 

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

R4822 
Conditional probability of the sample space 

R2203 
Expectation of poisson random basic natural number 

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

R3931 
Subtracting set from empty set 

R3471 
Open complex mapping theorem 

R1338 
Probabilistic BorelCantelli lemma 

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

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

R3946 
Interior is an open set 

R4512 


R2150 
Expectation of conditional expectation 

R4603 


R4908 
Strong derivative for affine euclidean real function 

R4208 


R1848 
Bijection between parenthesissliced cartesian products 

R5045 
Basic real matrix multiplied by column matrix from the right 

R4326 
Probability of binary union with almost sure event 

R4271 
Absolute value function is not strictly isotone 

R4513 


R3944 
Open set iff equal to interior 

R3618 
Turning two unsigned basic real numbers into convex combination coefficients 

R2950 
Complex conjugation operation is an involution 

R4873 


R3679 
Standardised I.I.D. real central limit theorem 

R4661 
Integer power recurrence of basic real golden ratio 

R2138 
Translation invariance of unsigned basic Lebesgue integral 

R2787 
Pascal's rule 

R1233 
Finite additivity of unsigned basic integral 

R4678 
Independent finite random basic real collection is uncorrelated 

R4783 


R5063 
Cofactor partition of determinant for real square matrix 

R4139 
Mill's inequalities 

R4378 
Independent random basic real pair iff distribution functions factorise 

R517 
Singletons are closed in Hausdorff space 

R2060 
Probability of set difference 

R1544 
Anova partition of orthogonal projection 

R399 
Injectivity is hereditary 

R1744 
Finite union of finite sets is finite 

R4074 
Arbitrary intersection of subsets is subset 

R3559 
Probability of random basic real number taking value in rightclosed interval 

R2548 
Constant map pulls back a bottom sigmaalgebra 

R1566 
Mean value theorem for Riemann integral 

R2535 
Chebyshov's inequality 

R4562 
Basic integral over a set of measure zero is zero 

R4391 
Characteristic function identifies distribution of random euclidean real number 

R4927 
Binary partition additivity of unsigned basic measure 

R4929 
Binary partition additivity of probability measure 

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

R4829 
Base inversion property of standard natural logarithm function 

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

R219 
Difference of set and intersection equals union of differences 

R4841 
Finite disjoint additivity of probability measure 

R2120 
Bounded continuous function is Riemann integrable on a basic real interval 

R983 
Sequential continuity of measure from above 

R3232 
Value of standard logarithm function at its parameter value 

R4095 
Basic real arithmetic expression for basic real arithmetic mean 

R3535 
Riemann integral of unit semicircle 

R3676 
Characteristic function for sum of independent random euclidean real numbers 

R4323 


R4468 
Set of stationary measurable sets is a sigmaalgebra 

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

R5094 
Number of boolean functions on a boolean cartesian product 

R4262 
Finite cartesian product with empty set is empty 

R3259 
Weak law of large numbers for variance with weighted decay 

R4534 


R2875 
Cauchy's basic real mean value theorem 

R4437 
Complement of stationary measurable set is stationary 

R2113 
Riemann integral of a constant function 

R4830 
Change of base formula for logarithm function 

R3843 
I.I.D. real central limit theorem 

R4754 


R1162 
Lebesgue sigmaalgebra is closed under reflections 

R76 
Empty set is closed 

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

R2466 
Real matrix determinant is multiplicative 

R2539 
Probabilistic Chebyshov's inequality 

R5061 
Expression of real matrix inverse in terms of adjugate 

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

R4931 


R4648 
Union of sigmaalgebras need not be a sigmaalgebra 

R2223 
Binary set union is commutative 

R560 
Division theorem in the ring of basic integers 

R756 
Abelian group iff centre is whole group 

R1276 
Every map from discrete topological space is continuous 

R3776 
Probability to win an exponential race 

R1831 
Real arithmetic expression for binomial coefficient 

R3061 
Basic Riemann integral over a reflected interval 

R1149 
Every point in open set is an interior point 

R3774 
Probability distribution function of exponential random basic number 

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

R4320 
Set of singletons is subset of power set 

R1514 
Isotonicity of signed basic integral 

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

R3938 
Upper and lower bounds for codomain set of probability measure 

R2933 
Isotonicity of convergent basic real series 

R4310 
Number of Nary relations on a finite set 

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

R716 
Equivalence class is not empty 

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

R2757 
Proper contraction map is continuous 

R4263 
Countable cartesian product with empty set is empty 

R4663 
Basic real square root function is subconvex 

R1372 
Inner product is zero if either argument is zero 

R738 
Left and right cosets coincide in Abelian group 

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

R4268 
Finite set union with empty set 

R3500 
Homomorphism property of the standard natural basic real exponential function 

R263 
Binary cartesian product of countable sets is countable 

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

R3325 
Banach fixed point theorem 

R4638 
Complexlinearity of complex matrix trace 

R4228 
Basic real ordering is compatible with addition 

R4216 
Finite set intersection is invariant under bijective shifting of indices 

R1743 
Intersection of finite sets is finite 

R4756 


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

R3228 
Bounded sequence need not be Cauchy 

R4887 
Cardinality of binary cartesian product of finite sets 

R4567 
Countable indicator partition of a random euclidean real number 

R3995 
Complex binomial theorem 

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

R3166 
Fourier transform of absolutely integrable function vanishes at infinity 

R1371 
Bilinear map is zero if either argument is zero 

R3562 
Basic real conditional variance partition into conditional moments 

R1194 
Indicator function with respect to set complement 

R4007 
Singletons are closed in Polish space 

R2595 
Convolution identity for binomial coefficient 

R4565 
Countable indicator partition of a euclidean real function 

R828 
First group isomorphism theorem 

R4832 
Homomorphism property of standard logarithm function in the binary case 

R2665 
Characteristic function of gaussian random real number 

R2014 
Triangle inequality for signed basic integral 

R4675 


R477 
Set finiteness is hereditary 

R355 
Inverse image of singleton set 

R466 
Principle of doublenegation is a propositional tautology 

R176 
Canonical set epimorphism is surjection 

R4112 
Strong fundamental theorem of complex algebra 

R2653 
Basic real conditional expectation is absolutely integrable 

R4617 
The standard mollifier integrates to one 

R26 
Pythagorean theorem 

R4928 
Finite partition additivity of probability measure 

R5079 
Characterisation of complex matrix eigenvalues in terms of characteristic polynomial 

R221 
Cartesian product is not associative 

R4845 
Joint entropy formula for simple mutual information 

R4055 
Singleton map is injection from set to power set 

R4849 
Symmetry of simple mutual information 

R2422 
Complexlinearity of Fourier transform 

R4188 
Set cardinality in terms of finite ambient set 

R3184 
Second fundamental theorem of Riemann integral calculus 

R2074 
Isotonicity of inverse image 

R90 
Complex function convolution is homogeneous to degree one 

R4763 
Set complement of map inverse image 

R2435 
Every complex number aside from zero has polar form 

R2395 
Subset of empty set is empty 

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

R3645 
Countable partition additivity of unsigned basic measure 

R1036 
Power set is closed under complements 

R309 
Leftinvertible map iff injection 

R3885 
Gaussian approximation to Poisson distribution 

R1030 
Sigmaalgebra is closed under countable intersections 

R4628 
Map to empty set is a surjection 

R4309 
Number of Nary relations on a finite cartesian product 

R2295 
Unit increment property of the gamma function 

R3956 
Expectation of random unsigned basic number by integrating tail probabilities 

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

R3953 
Two almost surely equal random basic real numbers are identically distributed 

R4285 
Standard natural basic real exponential function maps zero to one 

R4270 
Set union with empty set 

R3600 
Finite sum of independent Poisson random natural numbers is Poisson 

R3440 
Uniformly continuous map preserves Cauchy sequences 

R3719 
Probability of complement event 

R3945 
Set is a superset to its interior 

R4117 
Endpoint bounds for basic real linear combination 

R352 
Inverse image of image 

R4913 
Strong derivative for euclidean real quadratic form without translation 

R4222 
Quotienting a set reduces its cardinality 

R1565 
Goursat's theorem 

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

R4786 
Basic real conditional covariance partition into conditional moments 

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

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

R4489 
Sigmaalgebra is closed under limit superiors and limit inferiors 

R3844 
Characteristic function of scaled random basic real number 

R4900 


R30 
Inverse image of intersection is intersection of inverse images 

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

R3462 
Goursat's theorem for circles 

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

R2158 
Conditional expectation given independent sigmaalgebra 

R3921 
Identically distributed random collection need not be stationary 

R4079 
Modus tollendo ponens in propositional logic 

R4461 


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

R3960 
Identically distributed random variables need not be almost surely equal 

R3206 
Probability mass function for binomial random natural number 

R2254 
Riemann integral of pristine basic real gaussian function on the real line 

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

R4989 
Information inequality 

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

R4186 
Complement of a Gdelta set is an Fsigma set 

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

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

R4705 
Inner product with repeating argument is a basic real number 

R3883 
Rowstandardisation of rowindependent random basic real triangular array 

R2071 
Isotonicity of set union 

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

R4266 
Countable set intersection with empty set is empty 

R3316 
Pointwise limit of continuous functions need not be continuous 

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

R368 
Image of countable set is countable 

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

R4318 
Inclusionexclusion principle for unsigned basic measure of binary union 

R2168 
Isotonicity of Lebesgue outer measure 

R3415 
Necessary and sufficient condition for convergence of geometric complex series 

R3512 
Unsigned basic integral over set of measure zero is zero 

R2055 
Cavalieri principle for basic real Riemann integral calculus 

R424 
Euler's identity 

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

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

R1762 
Closed set less open set is closed 

R4867 
Initial sum of powers of two 

R4219 
Dirichlet's theorem 

R2374 
BorelCantelli zeroone law 

R4131 
Markov lower bound on unsigned basic expectation 

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

R17 
Bijective map from natural numbers to integers 

R4542 
Map is inverse to its inverse 

R2080 
Union is upper bound for intersection 

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

R3602 
Gaussian approximation to binomial distribution 

R1083 
Minimal element is minimum element in ordered set 

R4322 
Cardinality of finite set union of disjoint sets 

R2339 
Finite sum of uncorrelated basic real gaussians is basic real gaussian 

R74 
Finite union of closed sets is closed 

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

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