R3945 Set is a superset to its interior
R4294 Set difference with finite minuend is finite
R4329 Probability of countable intersection with an almost sure event
R4269 Countable set union with empty set
R4330 Probability of finite intersection with an almost sure event
R4165 Superset of countable union iff superset of every set in the union
R2740 Splitting a Riemann integral over an implicit interval partition
R3680 Characteristic function of standard gaussian random basic real number
R3719 Probability of complement event
R4598 Standard gaussian basic real density function is an even function
R2989 Unsigned basic Lebesgue integral under scaling
R3749 Decomposition of basic real square matrix into sum of symmetric and antisymmetric parts
R4541 Open set is its own interior
R4095 Basic real arithmetic expression for basic real arithmetic mean
R1885 Absolute value of basic function equals sum of positive and negative parts
R3416 Absolute value bounds for a basic real number
R4332
R2744 Square root of prime is irrational
R4455
R2897 Fourier transform under scaling
R2090 Isotonicity of probability measure
R4513
R4310 Number of N-ary relations on a finite set
R4073 Probability of union with impossible event
R4166 Superset of finite union iff superset of every set in the union
R4321 Set and set complement are disjoint
R1832 Cardinality of a finite cartesian product of finite sets
R4383 Euclidean real Fourier transform is uniformly bounded
R984 Transforming an isotone sequence of sets into pairwise disjoint sequence with common limit
R979 Countable subadditivity of measure
R4147 Not all subsets of a cartesian product need be cylinder sets
R301 Canonical identity map is injection
R125 Subset relation is reflexive
R1338 Probabilistic Borel-Cantelli lemma
R4463 Strongly mixing probability-preserving system is weakly mixing
R4171 Difference of set and countable union equals intersection of differences
R2963 Odd function equals its odd part
R4468 Set of stationary measurable sets is a sigma-algebra
R347 Isotonicity of map image
R517 Singletons are closed in Hausdorff space
R4577 Countable indicator partition of complex expectation in terms of pullback events
R4091 Biconditional boolean logic gate iff complement of trivial distance function on basic boolean ordered pairs
R714 Element belongs to its own equivalence class
R1603 De Moivre's theorem
R1012 Monotonicity of real limits
R2120 Bounded continuous function is Riemann integrable on a basic real interval
R3844 Characteristic function of scaled random basic real number
R4268 Finite set union with empty set
R1131 Image of inverse image
R1530 Inverse image preserves set difference
R1869 Characterisation of equality of maps
R3953 Two almost surely equal random basic real numbers are identically distributed
R88 Convolution is associative
R50 Set difference equals intersection with complement
R2220 Binary set intersection is commutative
R74 Finite union of closed sets is closed
R47 Set difference is subset of the minuend
R477 Set finiteness is hereditary
R2014 Triangle inequality for signed basic integral
R2075 Image of empty set
R4048 Number of binary relations on finite cartesian product
R4534
R4341 Bayes' theorem in the case of two pullback events
R4215 Countable set intersection is invariant under bijective shifting of indices
R4089 Sheffer basic boolean logic gate iff complement of minimum function on basic boolean ordered pairs
R4009 Metrisable topological space is Fréchet
R3201 Characteristic function of Binomial random natural number
R2413 Complex conjugate of real number
R2599 Cantor's theorem
R3508 Fermat's last theorem
R3908 Characteristic function of almost surely constant random euclidean real number
R3956 Expectation of random unsigned basic number by integrating tail probabilities
R4326 Probability of binary union with almost sure event
R4219 Dirichlet's theorem
R822 Group of prime order is cyclic
R3200 Characteristic function of Bernoulli random boolean number
R4648 Union of sigma-algebras need not be a sigma-algebra
R1577 Cauchy's theorem for a disc
R3205 Probability mass function for geometric random positive integer
R3938 Upper and lower bounds for codomain set of probability measure
R4011 Polish space is second-countable
R3367 Characterisation of convergence of geometric basic real series
R4159 Power set is not empty
R3586 Basic function is finite almost everywhere iff positive and negative parts are
R4391 Characteristic function identifies distribution of random euclidean real number
R102 Singletons are closed in a metric space
R1160 Reflection invariance of Euclidean volume function
R1743 Intersection of finite sets is finite
R4322 Cardinality of finite set union of disjoint sets
R3583 Random basic number absolutisation equals sum of positive and negative parts
R4591 Binary additivity of transpose for basic real matrices
R2653 Basic real conditional expectation is absolutely integrable
R4295 Power set of a countable set need not be countable
R4314 Number of basic boolean functions on a finite set
R2690 Minimum and maximum of stopping times are stopping times
R2060 Probability of set difference
R4007 Singletons are closed in Polish space
R2093 Countable subadditivity of probability measure
R4334 Every nonempty finite graph contains a bipartite subgraph with at least half the edges
R1450 Explicit algebraic expression for elements of generated subgroup
R2150 Expectation of conditional expectation
R221 Cartesian product is not associative
R4340 Bayes' theorem in the case of event and complement
R4538 Inclusion of image does not imply inclusion of inverse image
R2373 Second probabilistic Borel-Cantelli lemma
R3904 Characteristic function of Poisson random natural number
R1851 Cardinality of set of permutations on finite set
R4470 Inverse image of countable union is union of inverse images
R1177 Constant map is always measurable
R4350 Finite superadditivity of finite set cardinality
R4368 Set of euclidean integers has Lebesgue measure zero
R4338 Conditional probability of almost surely true event
R3516 Signed basic expectation of almost surely zero random number is zero
R4266 Countable set intersection with empty set is empty
R4543 Map inverse is invertible
R4630 Bijection between parenthesis-sliced cartesian triple products
R1165 Reflection invariance of Lebesgue measure
R4265 Finite set intersection with empty set is empty
R3215 Characteristic function of indicator random boolean number
R2158 Conditional expectation given independent sigma-algebra
R1372 Inner product is zero if either argument is zero
R76 Empty set is closed
R1839 Cardinality of power set of finite set
R4503 Countable union of sets of measure zero is of measure zero
R2339 Finite sum of uncorrelated basic real gaussians is basic real gaussian
R463 Law of the excluded middle is a propositional tautology
R2076 Inverse image of empty set
R352 Inverse image of image
R1194 Indicator function of complement
R4274 Absolute value function escapes to positive infinity in both directions
R1166 Lebesgue measure under scaling
R755 Group centre is Abelian group
R4563 Complex integral over a set of measure zero is zero
R1650 Interior point of set iff has open neighbourhood contained in set
R4158 Power set is multiplicative
R4293 Power set of a finite set is finite
R2071 Isotonicity of set union
R508 Finite cartesian product of countable sets is countable
R4518 Equivalent characterisations of finiteness of basic real variance
R465 De Morgan's laws are propositional tautologies
R4132 Strict version of probabilistic Markov inequality
R4187 Complement of an F-sigma set is a G-delta set
R4287 Finite product of even complex functions is even
R4157 Superadditivity of power set
R4143 Countable union is an upper bound to each set in the union
R447 Zorn's lemma
R1083 Minimal element is minimum element in ordered set
R4174 Proper contraction has at most a single fixed point
R4621 Standard mollifier is an approximate identity for complex Lebesgue convolution
R1488 Group is a subgroup of itself
R2422 Complex-linearity of Fourier transform
R3587 Random basic number almost surely finite iff positive and negative parts are
R4567 Countable indicator partition of a random euclidean real number
R1841 Indicator function operator is a bijection
R1234 Borel-Cantelli lemma
R2525 Independence of sigma-algebras is hereditary
R4511 Two complex numbers distinct iff difference distinct from zero
R1401 Orthogonality relation is a symmetric binary relation
R2081 Binary set intersection with empty set is empty
R4222 Quotienting a set reduces its cardinality
R2964 Even function equals its even part
R7 Empty set is subset of every set
R3912 Characteristic function of rademacher random basic integer
R4444 Superset differenced from set equals empty set
R4489 Sigma-algebra is closed under limit superiors and limit inferiors
R4280 Standard natural basic real exponential function is strictly isotone
R977 Ambient set is union of subset and complement of subset
R3789 Absolute value strictly less than real number iff in symmetric open interval
R4284 Standard natural basic real logarithm function escapes to negative infinity at zero
R4304 Nonempty finite poset contains a minimal element
R2203 Expectation of poisson random basic natural number
R1089 Characterisation of convergent sequences in metric space
R2270 Sigma-algebra is closed under symmetric differences
R2160 Conditional expectation of known random complex number
R4139 Mill's inequalities
R4607 Pushforward change of variables formula for unsigned basic integral
R262 Countable union of countable sets is countable
R4627
R4308 Map composition need not be commutative
R4172 Difference of set and finite union equals intersection of differences
R2262 Variance partition into first and second moments for random basic real number
R4325 Probability one if conditional probability one relative to event of probability one
R2595 Convolution identity for binomial coefficient
R4001 Whole space is clopen
R4500
R354 Image of singleton set
R4208
R2970 The four classes of basic real intervals are each closed under translation
R87 Convolution is commutative
R4333 Binary product of indicator functions equals indicator of intersection
R3935 Superset iff equal to union with subset
R2223 Binary set union is commutative
R4151 Binary intersection is a lower bound to each set in the union
R4378 Independent random basic real pair iff distribution functions factorise
R4486 Metric space is Hausdorff
R2522 Basic real conditional expectation with respect to a bottom sigma-algebra
R3971 Intersection of sets of infinite measure need not have infinite measure
R2966 Indicator function under scaling of the argument
R4464
R4267 Set intersection with empty set is empty
R3954 Two almost surely equal random variables are identically distributed
R4289 Vector space always has a basis
R1565 Goursat's theorem
R1906 Isotonicity of limits of basic real sequences
R1904 Isotonicity of finite basic real summation
R4162 Subset of finite intersection iff subset of every set in the intersection
R2310 Distribution formula for unsigned basic integral
R3969 Measure of intersection finite if measure of at least one set finite
R4610
R2254 Riemann integral of pristine basic real gaussian function on the real line
R4617 The standard mollifier integrates to one
R2615 Empty set is cofinite within a finite set
R4616 The standard mollifier satisfies sufficient conditions required of an approximate identity
R2141 Reflection invariance of unsigned basic Lebesgue integral
R3920 Sublevel events do not necessarily coincide for identically distributed random variables
R1036 Power set is closed under complements
R4596 Basic real calculus expression for moments of standard gaussian random basic real number
R4502 Difference of almost everywhere equal euclidean complex functions is almost everywhere zero
R3612 Standard natural basic real logarithm function is strictly isotone
R1077 Maximum element is unique
R2876 Basic mean value inequality
R4000 Empty set is clopen
R3946 Interior is an open set
R2929 Sum of odd functions is odd
R4281 Standard natural basic real exponential function is escapes to positive infinity at positive infinity
R4618 Riemann integral of standard basic real gaussian function on the real line
R244 Convergent sequence is Cauchy
R81 Bilipschitz map is continuous
R4573 Complex expectation over a null event is zero
R3512 Unsigned basic integral over set of measure zero is zero
R2437 Euclidean real Fourier inversion theorem
R4328 Probability of finite union with an almost sure event
R4456
R4536 Map image empty iff underlying set empty
R424 Euler's identity
R3206 Probability mass function for binomial random natural number
R3535 Riemann integral of unit semicircle
R4292 Finite cartesian product of finite sets is finite
R3970 Measure of finite union finite iff measure of all sets in union finite
R590 Square root of two is irrational
R4164 Superset of union iff superset of every set in the union
R716 Equivalence class is not empty
R3972 Expression for random basic real sum of squares in terms of sample mean and variance
R4580 Empty set union is the empty set
R457 Fréchet space iff singletons are closed
R4510 Two complex numbers equal iff difference equals zero
R2757 Proper contraction map is continuous
R4183 Alternative basic real arithmetic expressions for Catalan sequence
R1540 Affine map preserves convex sets in images
R2224 Set union is associative
R3843 I.I.D. basic real central limit theorem
R255 Power set of empty set
R4189
R2751 Fourier transform of absolutely integrable function is bounded
R4049 Number of binary relations on a finite set
R560 Division theorem in the ring of basic integers
R4331 Probability of binary intersection with an almost sure event
R4603
R4152
R2787 Pascal's rule
R4260 Basic real square root function is strictly isotone
R3515 Unsigned basic integral zero iff function almost everywhere zero
R4639 Characteristic function of translated random basic real number
R4542 Map is inverse to its inverse
R4163 Subset of binary intersection iff subset of both sets in the intersection
R4055 Singleton map is injection from set to power set
R893 Cyclic group is Abelian
R4013 Polish space is Fréchet
R4191
R2016 Probabilistic Markov's inequality
R2754 Lipschitz map is Hölder continuous
R983 Continuity of measure from above
R2741 Set equality iff inclusion in both directions
R4170 Difference of set and binary intersection equals union of differences
R1204 Fatou's lemma for unsigned basic integral
R1824 Birkhoff ergodic theorem
R4286 Standard natural basic real logarithm function maps one to zero
R4142 Union is an upper bound to each set in the union
R75 Intersection of closed sets is closed
R4438 Equivalent characterisations of ergodicity for probability-preserving system
R1120 Antitonicity of minimum
R1514 Isotonicity of signed basic integral
R1960 Characterisation of measure-preserving transformations by signed integral
R371 Countable set iff injection to natural numbers
R4443 Measure of symmetric difference of set and subset
R4339 Conditional probability of almost surely false event
R1975 Measure of set in backward orbit under measure-preserving endomorphism
R1762 Closed set less open set is closed
R1818 Isotonicity of basic real expectation
R975 Isotonicity of unsigned basic measure
R3640 Conditional probability given independent sigma-algebra
R2548 Constant map pulls back a bottom sigma-algebra
R1236 Markov's inequality
R3166 Fourier transform of absolutely integrable function vanishes at infinity
R756 Abelian group iff centre is whole group
R3038 Closed graph theorem
R4559 Probability of complement of an almost sure event
R10 Binary cartesian product with empty set is empty
R4012 Polish space is Hausdorff
R2871 Equivalent characterisations of a Schwartz function
R4088 Peirce basic boolean logic gate iff complement of maximum function on basic boolean ordered pairs
R4303 Nonempty finite poset contains a maximal element
R4320 Set of singletons is subset of power set
R1164 Translation invariance of Lebesgue measure
R2972 The four classes of basic real intervals are each closed under dilation
R4262 Finite cartesian product with empty set is empty
R4149 Countable intersection is a lower bound to each set in the union
R1744 Finite union of finite sets is finite
R2934 Isotonicity of unsigned basic real series
R1034 Power set is closed under unions
R4277 Measure of measurable set complement
R4093 Basic real harmonic and arithmetic means are multiplicative inverses when arguments are
R2100 Triangle inequality for signed basic expectation
R1170 Euclidean volume of singleton
R3983 Subcollection of independent collection of sigma-algebras is independent
R4010 Polish space is first-countable
R4270 Set union with empty set
R3942 Derivative of gaussian basic real density function
R24 Parallelogram identity
R3060 Basic Riemann integral of even function over an interval symmetric abour zero
R263 Binary cartesian product of countable sets is countable
R4445 Inclusion-exclusion principle for probability of binary union
R4182 Isotonicity of sublevel probabilities for random basic real number
R3513 Measurable subnull set has measure zero
R2786 Complement property of binomial coefficient
R1544 Anova partition of orthogonal projection
R511 Binary cartesian product of the set of natural numbers with itself is countable
R3974 Sum of independedent standard chi-squard random basic real numbers is chi-squared
R1959 Young's inequality
R1176 Inverse image of a constant map is either empty or equal to the domain set
R3595 Probabilistic Tonelli's theorem
R3192 I.I.D. sequence of standard gaussian random basic real numbers is standard gaussian random euclidean real number
R4583
R2386 Characterisation of almost sure convergence using limit superior and limit inferior
R2959 Function even part is even
R3532 Tautological pointwise lower bound from indicator function on sublevel set
R2079 Isotonicity of set intersection
R1076 Minimum element is unique
R978 Measure of set difference
R4657 Probability calculus expression for conditional probability given a finite partition of the sample space
R4145 Binary union is an upper bound to both sets in the union
R3506 Finite union of countable sets is countable
R4169 Difference of set and finite intersection equals union of differences
R2168 Isotonicity of Lebesgue outer measure
R3649 Expectation of conditional probability
R1064 Isotonicity of Lebesgue measure
R4437 Complement of stationary measurable set is stationary
R3896 Expectation is idempotent
R3641 Conditional probability given independent random variable
R298 Identity map is continuous if topology on domain set is equal or stronger
R1158 Translation invariance of Euclidean volume function
R4074 Arbitrary intersection of subsets is subset
R4566 Countable indicator partition of a complex function
R4661 Integer power recurrence of basic real golden ratio
R2062 Antitonicity of subtracting from the same set
R219 Difference of set and intersection equals union of differences
R1035 Power set is closed under intersections
R26 Pythagorean theorem
R2732 Kolmogorov zero-one law
R4609
R1838 Cardinality of finite set union of finite sets
R4327 Probability of countable union with an almost sure event
R2337 Density function for binary sum of independent random basic real numbers
R507 Empty set is countable
R2086 Finite inclusion-exclusion principle for unsigned basic measure
R4127 Basic real exponentiation function with unsigned exponent is isotone on unsigned basic reals
R4467 Empty set is a stationary measurable set
R2082 Binary set union with empty set
R3440 Uniformly continuous map preserves Cauchy sequences
R3529 Tautological pointwise inequality from indicator functions on sublevel sets
R4279 Explicit algebraic expression for elements of generated subgroup with singleton generator set
R1370 Multilinear map is zero if any argument is zero
R2368 I.I.D. strong law of large numbers
R4348 Two disjoint events are not necessarily independent
R3325 Banach fixed point theorem
R3784 Law of total probability for complex expectation in terms of pullback events of a discrete random variable
R2219 Set intersection is associative
R2089 Unsigned basic expectation is compatible with probability measure
R4090 Exclusively disjunctional boolean logic gate iff trivial distance function on basic boolean ordered pairs
R248 Binary subadditivity of basic real square root function
R4140 Standardised Mill's inequalities
R3679 Standardised I.I.D. basic real central limit theorem
R4318 Inclusion-exclusion principle for unsigned basic measure of binary union
R1022 Partition of basic function into positive and negative parts
R3479 Conformal complex function iff holomorphic bijection
R4160 Subset of intersection iff subset of every set in the intersection
R1149 Every point in open set is an interior point
R2748 Finite sets are closed in metric space
R3747 Transpose of finite product of finite basic real matrices
R3984 Subcollection of independent random collection is independent
R4604 Density partition for natural number moment of random basic real number
R4309 Number of N-ary relations on a finite cartesian product
R3919 Probability measure need not be an injection
R4214 Finite set union is invariant under bijective shifting of indices
R4211 Basic real golden ratio is limit of successive terms in the Fibonacci natural number sequence
R4272 Absolute value function is not strictly antitone
R3289 Sequence in product space is Cauchy iff each component sequence is Cauchy
R4430 Probability of event in backward orbit under probability-preserving endomorphism
R4278 Expression for probability of event in terms of complement event
R293 Open set less closed set is open
R4283 Standard natural basic real logarithm function escapes to positive infinity at positive infinity
R315 Composition of surjections is surjection
R2641 Martingale is constant in expectation
R4520 Complex conditional expectation is absolutely integrable
R3901 Domain of map to monoid equals union of kernel and support
R4565 Countable indicator partition of a euclidean real function
R2914 Cantor-Bernstein theorem
R3995 Complex binomial theorem
R2764 Canonical singleton map is bijection
R4483 Basic real number is zero iff equal to its reflection
R4118 Basic real arithmetic expression for unsigned basic real geometric mean
R4473 Almost idempotency of conditional expectation of random complex number
R3061 Basic Riemann integral over a reflected interval
R2221 Set intersection is invariant under bijective shifting of indices
R4282 Standard natural basic real exponential function vanishes at negative infinity
R176 Canonical set epimorphism is surjection
R4595 Basic real calculus expression for moments of centred gaussian random basic real number
R3922 Gaussian random basic real number is symmetric about its expectation
R1868 Composition of indicator function with set endomorphism
R1233 Finite additivity of unsigned basic integral
R3988 Expression for quadratic form of finite basic real square matrix in terms of symmetric part
R3944 Open set iff equal to interior
R1575 Goursat's theorem for rectangles
R1193 Finite product of indicator functions equals indicator of intersection
R4264 Cartesian product with empty set is empty
R4508 Two basic real numbers equal iff difference equals zero
R1159 Euclidean volume function under scaling
R2222 Set union is invariant under bijective shifting of indices
R4207
R4323
R4213 Countable set union is invariant under bijective shifting of indices
R738 Left and right cosets coincide in Abelian group
R4374 Integral factorisation on a binary product of basic real lebesgue measure spaces
R4540 Inverse map is a bijection
R2374 Borel-Cantelli zero-one law
R2080 Union is upper bound for intersection
R4315 Cardinality of a finite set raised to a finite power
R3923 Standard gaussian random basic real number is symmetric about zero
R3745 Basic real square matrix antisymmetric part is zero definite
R1903 Basic integral of almost everywhere zero function is zero
R1848 Bijection between parenthesis-sliced cartesian products
R4186 Complement of a G-delta set is an F-sigma set
R2745 The only subset of finite set with same cardinality is the ambient set itself
R981 Countably infinite measurable cover has measurable subcover
R3404 Bayes' theorem in the case of two events
R4317 Inclusion-exclusion principle for unsigned basic measure of ternary union
R2833 Nonempty set is singleton iff all elements equal each other
R4131 Markov lower bound on unsigned basic expectation
R3262 Dilations of unsigned tail probability converge to zero
R982 Continuity of measure from below
R4398
R2441 Reflection invariance of Lebesgue outer measure
R4150 Finite intersection is a lower bound to each set in the union
R4631 Cardinality of finite cartesian products is invariant under insertion of parentheses
R4485 Convergent sequence in metric space has unique limit point
R309 Left-invertible map iff injection
R1558 Second fundamental theorem of complex integral calculus
R1232 Tonelli's theorem for sums and integrals
R4161 Subset of countable intersection iff subset of every set in the intersection
R4086 Conditional basic boolean logic gate iff minimum function on basic boolean ordered pairs
R1973 Map composition is associative
R3544 Endpoint bounds for basic real arithmetic mean
R4568 Countable indicator partition of a random complex number
R4637
R2067 Subtracting empty set from set
R4447
R3783 Law of total probability for complex expectation in terms of pullback events
R3746 Transpose of binary product of finite basic real matrices
R3316 Pointwise limit of continuous functions need not be continuous
R292 Union is smallest upper bound
R3770 Product of finite basic real 2-by-2 matrix with its transpose
R3514 Unsigned basic expectation over set of probability zero is zero
R4649 Probability calculus expression for basic real conditional expectation given a countable partition of the sample space
R4092 Basic real arithmetic expression for basic real harmonic mean
R1171 Isotonicity of Euclidean volume function
R3960 Identically distributed random variables need not be almost surely equal
R468 Lagrange's theorem
R2074 Isotonicity of inverse image
R370 Countable set iff surjection from natural numbers
R310 Right-invertible map iff surjection
R1406 Collection of sets ordered by inclusion contains a maximal element
R3958 Intersecting subtrahend with minuend preserves set difference
R1564 Oriented complex curve integral of continuous function with a primitive on open set
R4349 Two disjoint events independent iff one is of probability zero
R3518 Partition of random basic number into positive and negative parts
R2182 Isotonicity of basic real sublevel sets
R2313 Expectation with dual probability distribution function
R3531 Pointwise product with indicator function is lower bound for unsigned basic function
R4275 Absolute value function is an even basic real function
R4431
R4228 Basic real ordering is compatible with addition
R4597 Centred gaussian basic real density function is an even function
R4495 Superconvex and superconvex basic real functions on open basic real interval are continuous
R4512
R3504 Erdős discrepancy problem
R2485 Expectation of geometric random basic positive integer
R80 Lipschitz map is continuous
R1371 Bilinear map is zero if either argument is zero
R3931 Subtracting set from empty set
R4611
R4261 Basic real binomial theorem for exponent two
R4602 Element in finite cartesian product iff components in images of canonical projections
R1856 Cardinality of the set of maps between finite sets
R2981 Riemann integral is particular case of Lebesgue integral
R4626 Strict isotonicity of basic Riemann integral
R4453 Probability of symmetric difference of event and subevent
R4615 Sufficient conditions to qualify as an approximate identity to complex Lebesgue convolution
R2377 Almost sure convergence implies convergence in probability
R4087 Disjunctional basic boolean logic gate iff maximum function on basic boolean ordered pairs
R399 Injectivity is hereditary
R3897 Distribution of random finite euclidean real sum is convolution of distribution measures
R246 Cauchy sequence is bounded
R4628 Map to empty set is a surjection
R2928 Finite sum of even euclidean real functions is even
R30 Inverse image of intersection is intersection of inverse images
R1073 Mean value theorem
R2665 Characteristic function of gaussian basic random number
R355 Inverse image of singleton set
R4291 Vector space always has an inclusion-maximal linearly independent set
R976 Finite disjoint additivity of unsigned basic measure
R466 Principle of double-negation is a propositional tautology
R2750 Fourier transform of finite unsigned euclidean real Borel measure is uniformly bounded
R4601 Element in countable cartesian product iff components in images of canonical projections
R3757 Linearity of basic real matrix trace
R4632 Cardinality of cartesian triple products is invariant under insertion of parentheses
R4562 Basic integral over a set of measure zero is zero
R4461
R4206 Basic real golden ratio is a root of a quadratic basic real polynomial
R2138 Translation invariance of unsigned basic Lebesgue integral
R2767 Identity map is injection
R4290 Vector space always has a linearly independent subset
R3605 Subadditivity of basic real square root function
R4188 Set cardinality in terms of finite ambient set
R1130 Intersection is largest lower bound
R49 Isotonicity of subtracting same set
R2537 Basic real exponentiation function with positive exponent is strictly isotone on positive basic reals
R2788 Basic real binomial theorem
R3517 Unsigned basic expectation zero iff random number almost surely zero
R220 Difference of set and union equals intersection of differences
R4288
R3621 Standard natural exponential function equals powers of Napier's constant
R1566 Mean value theorem for Riemann integral
R2746 Finite sets are closed in Fréchet space
R4173 Difference of set and binary union equals intersection of differences
R4369 Set of euclidean rational numbers has Lebesgue measure zero
R2112 Isotonicity of Riemann integral
R2405 Characteristic function identifies distribution of random basic real number
R1178 Continuous map is Borel measurable
R2960 Function odd part is odd
R3462 Goursat's theorem for circles
R1369 Jensen's inequality for expectation
R90 Complex function convolution is homogeneous to degree one
R3748 Finite basic real matrix is positive definite iff symmetric part is
R1030 Sigma-algebra is closed under countable intersections
R4370 Set of euclidean natural numbers has Lebesgue measure zero
R3228 Bounded sequence need not be Cauchy
R2370 Basic real arithmetic expression for cardinality of countable set
R4509 Two basic real numbers distinct iff difference distinct from zero
R2747 Finite sets are closed in Hausdorff space
R237 Intersection distributes over union
R4271 Absolute value function is not strictly isotone
R4560 Probability of complement of a null event
R4599 Density partition for expectation of random basic real number
R17 Bijective map from natural numbers to integers
R3911 Probability density function for standard gaussian random basic real number
R4148 Intersection is a lower bound to each set in the union
R4273 Absolute value function preserves zero
R2986 Lebesgue outer measure under scaling
R1846 Cardinality of set complement
R322 Image of projection map
R3921 Identically distributed random collection need not be stationary
R1242 Unsigned basic integral is compatible with measure
R4606
R4387 Characteristic function of standard Poisson random basic natural number
R4167 Superset of binary union iff superset of both sets in the union
R1902 Signed basic integral of almost everywhere equal functions
R648 Proportionally bounded linear map is Lipschitz
R4469 Countable union of stationary measurable sets is stationary
R4216 Finite set intersection is invariant under bijective shifting of indices
R3507 Binary union of countable sets is countable
R2933 Isotonicity of convergent basic real series
R4263 Countable cartesian product with empty set is empty
R3461 Holomorphic function with vanishing derivative on complex domain is constant
R1487 Ring is a subring of itself
R2395 Subset of empty set is empty
R2556 Probability calculus expression for probability conditioned on event of nonzero probability
R4390 Fourier transform characterises euclidean real probability measure
R3939 Upper and lower bounds for codomain set of finite unsigned basic measure
R4654 Probability calculus expression for basic real conditional expectation given a complement partition of the sample space
R2719 Affine majorant for the standard natural logarithm
R4638 Complex-linearity of complex matrix trace
R4276 Triangle inequality for absolute value function
R4466 Whole space is a stationary measurable set
R4144 Finite union is an upper bound to each set in the union
R4656 Probability calculus expression for conditional probability given a countable partition of the sample space
R4285 Standard natural basic real exponential function maps zero to one
R3898 Distribution of sum of two random euclidean real numbers is convolution of distribution measures
R4168 Difference of set and countable intersection equals union of differences
R3582 Signed expectation finite iff absolutely integrable random basic number
R1213 Linearity of unsigned basic integral
R2440 Translation invariance of Lebesgue outer measure
R3383 Stein's lemma
R4537 Inclusion of inverse image does not imply inclusion of image
R233 Whole space is closed