MeasurableSpace.cardinalMeasurableSet_le
theorem MeasurableSpace.cardinalMeasurableSet_le :
∀ {α : Type u} (s : Set (Set α)), Cardinal.mk ↑{t | MeasurableSet t} ≤ max (Cardinal.mk ↑s) 2 ^ Cardinal.aleph0
This theorem states that for any type `α` and any set `s` of sets of `α`, the cardinality of the set of all measurable sets is less than or equal to the maximum of the cardinality of `s` and 2, raised to the power of the smallest infinite cardinal (denoted as ℵ₀ in set theory). In other words, if a sigma-algebra (a collection of sets closed under countable unions and complements) is generated by a set of sets `s`, then the number of measurable sets (sets that are part of a sigma-algebra in a given measure space) in the sigma-algebra is at most `(max #s 2) ^ ℵ₀`.
More concisely: The cardinality of a sigma-algebra generated by a set of sets is at most 2^ℵ₀ if its size is infinite, or the maximum of its size and 2.
|
MeasurableSpace.cardinal_measurableSet_le_continuum
theorem MeasurableSpace.cardinal_measurableSet_le_continuum :
∀ {α : Type u} {s : Set (Set α)},
Cardinal.mk ↑s ≤ Cardinal.continuum → Cardinal.mk ↑{t | MeasurableSet t} ≤ Cardinal.continuum
This theorem states that for every type `α` and a particular set of sets `s` of type `α`, if the cardinal number (size) of `s` is less than or equal to the cardinality of the continuum (the size of the set of all real numbers), then the cardinal number of all measurable sets `t` (i.e., the sets in the sigma algebra generated by `s`) will also be less than or equal to the cardinality of the continuum. In other words, if the original set of sets `s` is of a size at most as large as that of the real numbers, the sigma algebra generated from `s` will have also at most the size of the set of real numbers.
More concisely: If `s` is a set of type `α` with cardinality less than or equal to the continuum, then the cardinality of the sigma algebra generated by `s` is also less than or equal to the continuum.
|
MeasurableSpace.cardinal_generateMeasurableRec_le
theorem MeasurableSpace.cardinal_generateMeasurableRec_le :
∀ {α : Type u} (s : Set (Set α)) (i : (Quotient.out (Cardinal.aleph 1).ord).α),
Cardinal.mk ↑(MeasurableSpace.generateMeasurableRec s i) ≤ max (Cardinal.mk ↑s) 2 ^ Cardinal.aleph0
This theorem states that for any type `α` and any set `s` of sets of `α`, at each step `i` of the inductive construction (where `i` is an element of the type associated with the first uncountable cardinal number), the cardinality of the set of measurable spaces generated recursively by `s` and `i` is bounded above by the maximum of the cardinality of `s` and 2, raised to the power of the smallest infinite cardinal (often denoted as `ℵ₀` in set theory). This means the size of our constructed set of measurable spaces grows at most exponentially as we continue the inductive process.
More concisely: For any type `α` and set `s` of sets of `α`, the cardinality of the set of measurable spaces generated recursively by `s` and `i` at each step `i` of the inductive construction is bounded above by the maximum of the cardinality of `s` and 2 raised to the power of the smallest infinite cardinal number.
|
MeasurableSpace.cardinal_generateMeasurable_le_continuum
theorem MeasurableSpace.cardinal_generateMeasurable_le_continuum :
∀ {α : Type u} {s : Set (Set α)},
Cardinal.mk ↑s ≤ Cardinal.continuum →
Cardinal.mk ↑{t | MeasurableSpace.GenerateMeasurable s t} ≤ Cardinal.continuum
The theorem `MeasurableSpace.cardinal_generateMeasurable_le_continuum` states that for any type `α` and a set `s` of sets of type `α`, if the cardinality of `s` is less than or equal to the cardinality of the continuum (which is $2^{\aleph_0}$), then the cardinality of the collection of all sets that are measurable with respect to the sigma-algebra generated by `s` is also less than or equal to the cardinality of the continuum. In other words, if the cardinality of a set of generators for a sigma-algebra is at most the size of the continuum, then the resulting sigma-algebra cannot have more than continuum many measurable sets.
More concisely: The cardinality of a sigma-algebra generated by a set of size less than or equal to the continuum has cardinality at most the continuum.
|
MeasurableSpace.generateMeasurable_eq_rec
theorem MeasurableSpace.generateMeasurable_eq_rec :
∀ {α : Type u} (s : Set (Set α)),
{t | MeasurableSpace.GenerateMeasurable s t} = ⋃ i, MeasurableSpace.generateMeasurableRec s i
The theorem `MeasurableSpace.generateMeasurable_eq_rec` states that for any type `α` and any set `s` of subsets of `α`, the set of all subsets `t` such that `t` is in the sigma-algebra generated by `s` is exactly the union over all `i` of the sigma-algebras generated recursively by `s` and `i`. Essentially, it is stating that the process of generating the smallest sigma-algebra containing `s` can be formulated recursively.
More concisely: The sigma-algebra generated by a set `s` of subsets of a type `α` is equal to the union of the sigma-algebras generated recursively by `s` and each element in `s`.
|
MeasurableSpace.cardinal_generateMeasurable_le
theorem MeasurableSpace.cardinal_generateMeasurable_le :
∀ {α : Type u} (s : Set (Set α)),
Cardinal.mk ↑{t | MeasurableSpace.GenerateMeasurable s t} ≤ max (Cardinal.mk ↑s) 2 ^ Cardinal.aleph0
This theorem states that for any type `α` and any set `s` of subsets of `α`, the cardinality of the sigma-algebra generated by `s` is at most the maximum of the cardinality of `s` and 2, raised to the power of the smallest infinite cardinal (`ℵ₀`). In other words, the size of the sigma-algebra (the collection of measurable sets) generated by `s` is bounded above by `(max #s 2) ^ ℵ₀`.
More concisely: The cardinality of the sigma-algebra generated by a set of subsets of a type is strictly less than or equal to (1 + the maximum number of subsets) raised to the power of the smallest infinite cardinal.
|