ThmDex
Definitions
,
Results
,
Conjectures
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
Row-standardisation of row-independent random basic real standard triangular array
R3060
Basic Riemann integral of even function over an interval symmetric abour zero
R2914
Cantor-Bernstein 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 sigma-algebras is independent
R3494
Glivenko-Cantelli theorem
R5093
Total number of fixed-length 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 probability-preserving 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 sigma-algebra
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 measure-preserving 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
Inclusion-exclusion 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
Right-invertible 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ér-Wold 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 second-countable
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 Borel-Cantelli lemma
R2788
Real binomial theorem
R50
Set difference equals intersection with complement
R4895
Standard counting measure is a point-mass measure
R25
Cauchy-Schwarz 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 probability-preserving system is weakly mixing
R3922
Gaussian random basic real number is symmetric about its expectation
R4871
Translation property of the standard log-sum-exp 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 chi-squard random basic real numbers is chi-squared
R4598
Standard gaussian basic real density function is an even function
R4630
Bijection between parenthesis-sliced 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
First-degree 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 sigma-algebra
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 Moivre-Laplace 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 F-sigma set is a G-delta set
R1975
Measure of set in backward orbit under measure-preserving 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
Sigma-algebra 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 zero-one 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
Borel-Cantelli 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
Inclusion-exclusion 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 non-null 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 self-dot product function
R3770
Product of finite basic real 2-by-2 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 real-valued
R2938
Vanishing sequence is necessary for finiteness of real series
R4973
Bias-variance partition of mean square error for random basic real number
R2525
Independence of sigma-algebras 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 inclusion-exclusion 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
Inclusion-exclusion 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 chi-squared 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 arithmetic-geometric 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 multiplicative-additive 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
Bias-variance 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 N-subsets 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 inclusion-maximal linearly independent set
R4430
Probability of event in backward orbit under probability-preserving 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 geometric-harmonic 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 GM-HM inequality
R4010
Polish space is first-countable
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 non-null 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
Inclusion-exclusion 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 sigma-algebra 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 2-by-2 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 Borel-Cantelli 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 parenthesis-sliced 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 right-closed interval
R2548
Constant map pulls back a bottom sigma-algebra
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 sigma-algebra
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 sigma-algebra 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 sigma-algebras need not be a sigma-algebra
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 N-ary 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
Complex-linearity 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
First-degree 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 double-negation 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
Complex-linearity 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
Left-invertible map iff injection
R3885
Gaussian approximation to Poisson distribution
R1030
Sigma-algebra is closed under countable intersections
R4628
Map to empty set is a surjection
R4309
Number of N-ary 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
Sigma-algebra 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 sigma-algebra
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 G-delta set is an F-sigma 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
Row-standardisation of row-independent 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
Inclusion-exclusion 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
Borel-Cantelli zero-one 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