Definitions
,
Results
,
Conjectures
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
First-degree 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 real-linearly 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 sigma-algebra 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 non-null 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 first-countable
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 real-linearly 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
Complex-linearity 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
Bias-variance 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
Complex-linearity 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 3-by-3 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
Inclusion-exclusion 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 probability-preserving 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 left-closed unit interval iff infinite product of duals does not vanish
R4338
Conditional probability of almost surely true event
R4610
R3633
Bessel-corrected 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 two-dimensional 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
Row-standardisation of row-independent 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
Cauchy-schwarz 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 N-ary relations on a finite cartesian product
R5595
Positive definite complex square matrix is conjugate symmetric
R1975
Measure of set in backward orbit under measure-preserving 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 non-null 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 first-order 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
Complex-linearity 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
Inclusion-exclusion 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 3-by-3 real square matrix
R5306
Conditional expectation of a random complex matrix given minimal information
R3559
Probability of random real number taking value in right-closed 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ér-Wold theorem
R4903
Strong derivative for affine basic real function
R25
Cauchy-Schwarz 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 N-ary 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 self-dot 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 real-valued
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 left-closed 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 AM-GM 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
Complex-linearity 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
Cauchy-Schwarz 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 zero-one 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 Moivre-Laplace 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 sigma-algebra
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
Mean-median-mode 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 left-closed 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
Sigma-algebra 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 sigma-algebra is closed under reflections, translations, and scaling
R4908
Strong derivative for affine euclidean real function
R112
Cavalieri principle
R3494
Glivenko-Cantelli 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 Cauchy-Schwarz 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 sigma-algebras need not be a sigma-algebra
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 sigma-algebra
R5230
Bessel-corrected sample variance of I.I.D. gaussians is a transformed chi-squared 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
Left-invertible map iff injection
R2302
Memorylessness property of exponential random positive real number
R5303
Real-linearity 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
Cantor-Bernstein 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 sigma-algebras 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 chi-squard random real numbers is chi-squared
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
First-degree 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 probability-preserving 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 log-sum-exp 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 second-countable
R2373
Second probabilistic Borel-Cantelli 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
Mean-deviance standardisation of a random real number
R4012
Polish space is Hausdorff
R5520
Cofactor partition for a 2-by-2 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 measure-preserving 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 2-by-2 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 sigma-algebras 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
Inclusion-exclusion 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 2-by-2 matrix with its transpose
R4780
Real conditional expectation given independent sigma-algebra
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
Inclusion-exclusion 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 point-mass 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 self-dot 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 2-by-2 real square matrix
R5359
Reflection property of simple relative entropy
R4756
R5229
Bessel-corrected sample variance of independent standard gaussians is a transformed chi-squared 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
Borel-Cantelli 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
Right-invertible 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 inclusion-exclusion 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
Sigma-algebra 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 sigma-algebra
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 2-by-2 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 N-subsets 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 right-closed unit interval vanishes iff infinite sum of duals diverges
R1558
Second fundamental theorem of complex integral calculus
R4187
Complement of an F-sigma set is a G-delta 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 probability-preserving endomorphism
R2079
Isotonicity of set intersection
R5093
Total number of fixed-length 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 G-delta set is an F-sigma 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 2-by-2 complex square matrix
R4666
Real GM-HM 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 log-sum-exp method
R4398
R4489
Sigma-algebra is closed under limit superiors and limit inferiors
R4074
Arbitrary intersection of subsets is subset
R5521
Signs of length-2 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 sigma-algebra
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 chi-squared 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 chi-squared 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 2-by-2 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 2-by-2 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
Inclusion-exclusion lower bound to probability of ternary intersection
R4973
Bias-variance partition of mean square error for random basic real number
R4740
R4157
Superadditivity of power set
R466
Principle of double-negation is a propositional tautology
R5192
Cauchy-Schwarz 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 parenthesis-sliced 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 parenthesis-sliced 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
Complex-linearity 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
Mean-value 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 sigma-algebra
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 inclusion-maximal 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
Row-standardisation of row-independent 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
Borel-Cantelli zero-one 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 GM-HM 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 Borel-Cantelli 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 right-closed 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 AM-GM 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