nonempty_measurable_superset
theorem nonempty_measurable_superset :
∀ {α : Type u_1} {m : MeasurableSpace α} (s : Set α), Nonempty { t // s ⊆ t ∧ MeasurableSet t }
The theorem `nonempty_measurable_superset` states that for any type `α` and for any `MeasurableSpace` on `α`, every set `s` of type `α` has a superset `t` that is measurable. In other words, it's always possible to find a measurable set `t` that includes `s` as a subset. Here, the notation `{ t // s ⊆ t ∧ MeasurableSet t }` represents the set of all such supersets `t` of `s` that are measurable. The `Nonempty` term indicates that this set of supersets is not empty - meaning that at least one such superset exists.
More concisely: For any type `α` and MeasurableSpace on `α`, every subset `s` of `α` has a measurable superset.
|
Mathlib.MeasureTheory.MeasurableSpace.Defs._auxLemma.1
theorem Mathlib.MeasureTheory.MeasurableSpace.Defs._auxLemma.1 :
∀ {α : Type u_1} [inst : MeasurableSpace α], MeasurableSet ∅ = True
The theorem `Mathlib.MeasureTheory.MeasurableSpace.Defs._auxLemma.1` states that for all types `α` that have an associated `MeasurableSpace` structure, the empty set `∅` is a measurable set. In other words, in the context of measure theory, the empty set is always considered measurable regardless of the space we are working in.
More concisely: The empty set is measurable in any measurable space.
|
MeasurableSet.const
theorem MeasurableSet.const : ∀ {α : Type u_1} {m : MeasurableSpace α} (p : Prop), MeasurableSet {_a | p}
The theorem `MeasurableSet.const` states that for any type `α` and any measurable space `m` defined over `α`, any set that is defined by a constant proposition `p` (i.e., a proposition that does not depend on the elements of the set) is a measurable set. This means the measurability criterion is satisfied by such sets, regardless of the actual proposition `p`.
More concisely: A constant proposition `p` defines a measurable set in a measurable space `m` over type `α`.
|
MeasurableSet.sInter
theorem MeasurableSet.sInter :
∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)},
s.Countable → (∀ t ∈ s, MeasurableSet t) → MeasurableSet s.sInter
This theorem states that for any type `α` and any measurable space `m` over `α`, if we have a countable collection `s` of sets of `α`, and each of these sets is measurable, then the intersection of all the sets in `s` is also a measurable set. In other words, the intersection of a countable collection of measurable sets is itself a measurable set. This theorem holds in the context of measure theory, which deals with concepts such as measurable spaces and sets.
More concisely: In measure theory, the intersection of any countable collection of measurable sets is a measurable set.
|
MeasurableSpace.measurableSet_empty
theorem MeasurableSpace.measurableSet_empty : ∀ {α : Type u_7} (self : MeasurableSpace α), self.MeasurableSet' ∅ := by
sorry
This theorem states that for any measurable space `α`, the empty set is a measurable set within that space. Here, `α` can be any type. The specific measurable space is represented by `self`. The theorem advises to use `MeasurableSet.empty` for this proof.
More concisely: The empty set is a measurable subset of any measurable space.
|
MeasurableSpace.measurableSet_compl
theorem MeasurableSpace.measurableSet_compl :
∀ {α : Type u_7} (self : MeasurableSpace α) (s : Set α), self.MeasurableSet' s → self.MeasurableSet' sᶜ
This theorem states that for any given type `α`, for any measurable space defined over `α`, and for any set `s` of elements of `α`, if `s` is a measurable set within this measurable space, then its complement `sᶜ` is also a measurable set within this same measurable space. In other words, the complement of a measurable set is always also a measurable set in any given measurable space. This theorem is essentially about the properties of measurable spaces, and it advises the use of `MeasurableSet.compl` for this purpose.
More concisely: If `s` is a measurable set in a measurable space over type `α`, then the complement `sᶜ` is also a measurable set in that measurable space.
|
MeasurableSingletonClass.measurableSet_singleton
theorem MeasurableSingletonClass.measurableSet_singleton :
∀ {α : Type u_7} [inst : MeasurableSpace α] [self : MeasurableSingletonClass α] (x : α), MeasurableSet {x} := by
sorry
This theorem states that a singleton, which is a set containing only one element, is a measurable set. Here, the term "measurable" is defined in the context of a given measurable space. More specifically, for any type `α` equipped with a measurable space structure and a measurable singleton class structure, any singleton set `{x}` (where `x` is an element of `α`) is measurable.
More concisely: In a measurable space with type `α` and measurable singleton class structure, every singleton set `{x}` is measurable.
|
measurable_const
theorem measurable_const :
∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {a : α}, Measurable fun x => a
The theorem `measurable_const` states that for any two types `α` and `β`, and for any measurable spaces `x` on `α` and `x_1` on `β`, and for any element `a` of type `α`, the constant function that maps every element of the domain to `a` is a measurable function. In other words, if we have a measurable space structure on two types `α` and `β`, and an element `a` of type `α`, then the function which assigns `a` to each element of `β` is a measurable function.
More concisely: For any measurable spaces (X, Σ) on type α and (Y, Σ₁) on type β, and any element a of α, the constant function mapping every element of Y to a is measurable.
|
measurable_id
theorem measurable_id : ∀ {α : Type u_1} {x : MeasurableSpace α}, Measurable id
The theorem `measurable_id` states that the identity function is measurable for all measurable spaces. In more formal terms, given any type `α` and a measurable space `x` over that type, the identity function (which maps each element of the space to itself) is a measurable function. This is defined as: for any measurable set in the codomain, its preimage under the identity function is also a measurable set.
More concisely: The identity function is measurable with respect to any measurable space.
|
MeasurableSpace.generateFrom_induction
theorem MeasurableSpace.generateFrom_induction :
∀ {α : Type u_1} (p : Set α → Prop) (C : Set (Set α)),
(∀ t ∈ C, p t) →
p ∅ →
(∀ (t : Set α), p t → p tᶜ) →
(∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n)) → p (⋃ i, f i)) → ∀ {s : Set α}, MeasurableSet s → p s
This theorem is about the properties of a measurable set in the measurable space. It's named `MeasurableSpace.generateFrom_induction` and it states that for any type `α`, any property `p` of sets of `α`, and any collection `C` of sets of `α`, if all elements in `C` have the property `p`, the empty set has the property `p`, the complement of any set having property `p` also has the property `p`, and any countable union of sets having the property `p` also has the property `p`, then any measurable set also has the property `p`. This implies that the property `p` is preserved under these operations common in measure theory, and that measurable sets are the smallest class of sets closed under these operations.
More concisely: If a collection of sets in a measurable space is closed under the operations of emptiness, complement, and countable union, then any measurable set belongs to this collection.
|
MeasurableSet.union
theorem MeasurableSet.union :
∀ {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α},
MeasurableSet s₁ → MeasurableSet s₂ → MeasurableSet (s₁ ∪ s₂)
The theorem `MeasurableSet.union` states that for any type `α`, given a measurable space `m` over `α`, and two sets `s₁` and `s₂` of type `α`, if both `s₁` and `s₂` are measurable sets in the given measurable space, then the union of `s₁` and `s₂` is also a measurable set in the same measurable space. This means that measurability is preserved under the set union operation.
More concisely: For any measurable space `m` over type `α`, if `s₁` and `s₂` are measurable sets in `m`, then their union `s₁ ∪ s₂` is also a measurable set in `m`.
|
MeasurableSpace.ext
theorem MeasurableSpace.ext :
∀ {α : Type u_1} {m₁ m₂ : MeasurableSpace α}, (∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s) → m₁ = m₂ := by
sorry
This theorem, `MeasurableSpace.ext`, states that for any type `α` and any two measurable spaces `m₁` and `m₂` over this type, if for every set `s` of elements of type `α`, `s` is measurable in `m₁` if and only if it is measurable in `m₂`, then `m₁` and `m₂` must be the same measurable space. In other words, two measurable spaces are equal if they agree on the measurability of every set.
More concisely: If two measurable spaces over the same type have identical measurability properties for every set, then they are equal.
|
Set.Finite.measurableSet
theorem Set.Finite.measurableSet :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSingletonClass α] {s : Set α},
s.Finite → MeasurableSet s
This theorem states that for any type `α` with a measurable space structure and a measurable singleton class structure, any finite set `s` of type `α` is also a measurable set. In other words, given a finite set in a measurable space, we can always regard it as a measurable set. This is achieved under the assumption that the singletons (sets with only one element) in the space are measurable.
More concisely: Given a measurable space `(α, Σ)` with measurable singletons, every finite set `s ⊆ α` belongs to `Σ`.
|
MeasurableSet.inter
theorem MeasurableSet.inter :
∀ {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α},
MeasurableSet s₁ → MeasurableSet s₂ → MeasurableSet (s₁ ∩ s₂)
The theorem `MeasurableSet.inter` states that for any type `α` and any measurable space `m` on `α`, if `s₁` and `s₂` are sets of `α` both of which are measurable sets, then their intersection `s₁ ∩ s₂` is also a measurable set. In terms of measure theory, it means that the intersection of any two measurable sets within a given measurable space is also a measurable set.
More concisely: If `α` is a type with a measurable space `m`, and `s₁` and `s₂` are measurable sets in `α` according to `m`, then `s₁ ∩ s₂` is also a measurable set according to `m`.
|
MeasurableSet.singleton
theorem MeasurableSet.singleton :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSingletonClass α] (a : α), MeasurableSet {a} := by
sorry
The theorem `MeasurableSet.singleton` states that for any type `α` equipped with a measurable space structure and a measurable singleton class structure, every singleton set of `α` is measurable. In other words, if we pick any element `a` from type `α`, the set containing only `a` (`{a}`) is measurable in the given measurable space of `α`.
More concisely: For any measurable space and measurable singleton class structure on type `α`, the singleton set `{a}` is measurable for all `a : α`.
|
Finset.measurableSet_biInter
theorem Finset.measurableSet_biInter :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} (s : Finset β),
(∀ b ∈ s, MeasurableSet (f b)) → MeasurableSet (⋂ b ∈ s, f b)
The theorem `Finset.measurableSet_biInter` states that for any types `α` and `β`, given a measurable space `m` over `α`, a function `f` from `β` to the set of `α`, and a finite set `s` of `β`, if every set `f(b)` with `b` belonging to `s` is measurable, then the intersection of all these sets `f(b)` is also measurable.
In mathematical terms, this theorem says that if $f : \beta \rightarrow \text{Set}\, \alpha$ is a function where $\forall b \in s$, $f(b)$ is measurable, then $\bigcap_{b \in s} f(b)$ is also measurable in the same measure space on `α`.
More concisely: If `f : β -> Set α` is a function such that for every `b` in a finite set `s` from `β`, `f(b)` is measurable in the measure space on `α`, then the intersection of all `f(b)` for `b` in `s` is measurable in the same measure space on `α`.
|
Finset.measurableSet
theorem Finset.measurableSet :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSingletonClass α] (s : Finset α),
MeasurableSet ↑s
The theorem `Finset.measurableSet` states that for any given finite set `s` of elements of type `α`, if `α` forms a measurable space and a measurable singleton class, then the set `s` is a measurable set. Here, "measurable" means that it can be meaningfully assigned a measure in the ambient measure space defined over `α`.
More concisely: If `α` is a measurable space and a measurable singleton class, then any finite set `s` of elements of type `α` is a measurable set.
|
MeasurableSet.diff
theorem MeasurableSet.diff :
∀ {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α},
MeasurableSet s₁ → MeasurableSet s₂ → MeasurableSet (s₁ \ s₂)
The theorem `MeasurableSet.diff` is a declaration that for any given type `α`, any given measurable space `m` over `α`, and any two sets `s₁` and `s₂` of type `α`, if `s₁` and `s₂` are both measurable sets, then the set difference `s₁ \ s₂` (the set of all elements that belong to `s₁` but not to `s₂`) is also a measurable set.
More concisely: If `m` is a measurable space on type `α`, and `s₁` and `s₂` are measurable sets in `α` with respect to `m`, then their set difference `s₁ \ s₂` is also a measurable set in `α` with respect to `m`.
|
DiscreteMeasurableSpace.forall_measurableSet
theorem DiscreteMeasurableSpace.forall_measurableSet :
∀ {α : Type u_7} [inst : MeasurableSpace α] [self : DiscreteMeasurableSpace α] (s : Set α), MeasurableSet s := by
sorry
This theorem, titled `DiscreteMeasurableSpace.forall_measurableSet`, states that for any type `α` and any set `s` of type `α`, given that `α` is equipped with a `MeasurableSpace` instance and a `DiscreteMeasurableSpace` instance, the set `s` is a measurable set. However, it is recommended not to use this theorem directly; instead, use `measurableSet_discrete`. The theorem is a property of discrete measurable spaces, which are a particular kind of measurable space, and it asserts that all sets in such a space are inherently measurable.
More concisely: In a discrete measurable space, every subset is measurable.
|
MeasurableSet.symmDiff
theorem MeasurableSet.symmDiff :
∀ {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α},
MeasurableSet s₁ → MeasurableSet s₂ → MeasurableSet (symmDiff s₁ s₂)
The theorem `MeasurableSet.symmDiff` states that for any type `α` equipped with a measurable space, and any two sets `s₁` and `s₂` of type `α`, if `s₁` and `s₂` are measurable sets, then the symmetric difference of `s₁` and `s₂` is also a measurable set. The symmetric difference of two sets `A` and `B` is defined as `(A \ B) ∪ (B \ A)`, where `\` denotes set difference and `∪` denotes the union of two sets.
More concisely: If `α` is a type with a measurable structure and `s₁` and `s₂` are measurable subsets of `α`, then the symmetric difference `(s₁ \ s₂) ∪ (s₂ \ s₁)` is a measurable subset of `α`.
|
Measurable.comp
theorem Measurable.comp :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {x : MeasurableSpace α} {x_1 : MeasurableSpace β}
{x_2 : MeasurableSpace γ} {g : β → γ} {f : α → β}, Measurable g → Measurable f → Measurable (g ∘ f)
The theorem `Measurable.comp` states that for all types `α`, `β`, and `γ` and for all measurable spaces over these types, if we have a function `g` from `β` to `γ` and a function `f` from `α` to `β` such that both `g` and `f` are measurable, then the composition of `g` and `f` (denoted by `g ∘ f`) is also measurable. In other words, the measurability property is preserved under function composition.
More concisely: If `f` from `α` to `β` and `g` from `β` to `γ` are measurable functions, then their composition `g ∘ f` is also a measurable function.
|
MeasurableSet.iUnion
theorem MeasurableSet.iUnion :
∀ {α : Type u_1} {ι : Sort u_6} {m : MeasurableSpace α} [inst : Countable ι] ⦃f : ι → Set α⦄,
(∀ (b : ι), MeasurableSet (f b)) → MeasurableSet (⋃ b, f b)
This theorem, `MeasurableSet.iUnion`, states that for any type `α`, index type `ι`, and measure space `m` on `α`, if `ι` is countable and `f` is a function from `ι` to the set of `α` such that every set `f b` for each `b` in `ι` is measurable, then the union of all such sets `f b` is also a measurable set. In mathematical terms, if $\{f(b): b \in \mathbb{N}\}$ is a collection of measurable sets, then $\bigcup_{b \in \mathbb{N}} f(b)$ is also a measurable set.
More concisely: If `ι` is countable and `f:` `ι` → `MeasurableSet α m` for a measure space `m` on type `α`, then `⋃b in ι. f b` is a measurable set.
|
MeasurableSpace.measurableSet_iUnion
theorem MeasurableSpace.measurableSet_iUnion :
∀ {α : Type u_7} (self : MeasurableSpace α) (f : ℕ → Set α),
(∀ (i : ℕ), self.MeasurableSet' (f i)) → self.MeasurableSet' (⋃ i, f i)
The theorem `MeasurableSpace.measurableSet_iUnion` states that for any arbitrary type `α` and any `MeasurableSpace` defined on this type, if we have a sequence of sets that are all measurable, then the union of all these sets (taken over all natural numbers) is also a measurable set. This theorem is a specific case of a more general theorem `MeasurableSet.iUnion`. This theorem essentially asserts that the process of forming a union preserves measurability.
More concisely: For any MeasurableSpace over type α and any sequence of measurable sets, their union is also measurable.
|
measurable_id'
theorem measurable_id' : ∀ {α : Type u_1} {x : MeasurableSpace α}, Measurable fun a => a
The theorem `measurable_id'` states that, for any given type `α` and any measurable space `x` of type `α`, the identity function (that is, a function which returns its input unchanged) is measurable. In mathematical terms, this means that for any measurable set within this space, the preimage of the set under the identity function is also measurable.
More concisely: The identity function is measurable, i.e., for any measurable set in a measurable space, its preimage under the identity function is also measurable.
|
MeasurableSet.univ
theorem MeasurableSet.univ : ∀ {α : Type u_1} {m : MeasurableSpace α}, MeasurableSet Set.univ
The theorem `MeasurableSet.univ` states that for any type `α` and any measurable space `m` on `α`, the universal set of `α` is measurable. In mathematical terms, if we consider a measure space on a given set, the entire set (which corresponds to the universal set in set theory) is always considered a measurable set. In the context of this theorem, a measurable set is a set for which we are able to accurately define its measure.
More concisely: For any measurable space `m` on type `α`, the universal set of `α` is measurable.
|
MeasurableSet.empty
theorem MeasurableSet.empty : ∀ {α : Type u_1} [inst : MeasurableSpace α], MeasurableSet ∅
The theorem `MeasurableSet.empty` states that for any type `α` in a measurable space, the empty set is a measurable set. In other words, regardless of the measurable space we are working in, the empty set is always considered measurable.
More concisely: In any measurable space, the empty set is a measurable subset.
|
MeasurableSpace.generateFrom_mono
theorem MeasurableSpace.generateFrom_mono :
∀ {α : Type u_1} {s t : Set (Set α)}, s ⊆ t → MeasurableSpace.generateFrom s ≤ MeasurableSpace.generateFrom t := by
sorry
This theorem states that for any type `α` and any two sets `s` and `t` of sets of `α`, if `s` is a subset of `t`, then the measurable space generated from `s` is less than or equal to the measurable space generated from `t`. In other words, if we add more basic sets to the collection from which we generate a measurable space, we cannot decrease the size of the measurable space. Rather, it will either stay the same or increase. This makes intuitive sense as adding more basic sets potentially allows more sets to be measurable.
More concisely: If `α` is a type and `s` is a subset of `t` are sets of `α`, then the measurable space generated from `s` is less than or equal to the measurable space generated from `t`.
|
MeasurableSet.biUnion
theorem MeasurableSet.biUnion :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} {s : Set β},
s.Countable → (∀ b ∈ s, MeasurableSet (f b)) → MeasurableSet (⋃ b ∈ s, f b)
The theorem `MeasurableSet.biUnion` states that for any types `α` and `β`, given a measure space `m` over `α`, a function `f` from `β` to a set of `α`, and a countable set `s` of `β`, if every set `f(b)` for all `b` in `s` is measurable, then the union of all `f(b)` for all `b` in `s` is also measurable. In simple terms, this theorem allows us to assert that if we have a countable collection of measurable sets, the union of this collection is also measurable.
More concisely: If `m` is a measure space over `α`, `f` is a function from `β` to `α`, and `s` is a countable set of `β` such that every `f(b)` is measurable for all `b` in `s`, then the union of all `f(b)` for `b` in `s` is measurable.
|
Mathlib.MeasureTheory.MeasurableSpace.Defs._auxLemma.2
theorem Mathlib.MeasureTheory.MeasurableSpace.Defs._auxLemma.2 :
∀ {α : Type u_1} {s : Set α} {m : MeasurableSpace α}, MeasurableSet sᶜ = MeasurableSet s
This theorem states that for any type `α`, any set `s` of type `α`, and any measurable space `m` of type `α`, the complement of `s` is a measurable set if and only if `s` is a measurable set. In mathematical terms, given a measurable space `m` on a type `α`, the complement (denoted by `sᶜ`) of a set `s` in `α` is measurable if `s` itself is measurable.
More concisely: For any measurable space `m` on type `α`, the complement of a measurable set `s` in `α` is also measurable.
|
MeasurableSet.biInter
theorem MeasurableSet.biInter :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} {s : Set β},
s.Countable → (∀ b ∈ s, MeasurableSet (f b)) → MeasurableSet (⋂ b ∈ s, f b)
The theorem `MeasurableSet.biInter` states that for any types `α` and `β`, any measurable space `m` on `α`, any function `f` from `β` to a set of `α`, and any set `s` of `β`, if the set `s` is countable and for every element `b` in `s` the set `f(b)` is measurable, then the intersection of all `f(b)` for `b` in `s` is also a measurable set. In other words, the countable intersection of measurable sets is measurable.
More concisely: If `m` is a measurable space on `α`, `f` is a function from `β` to `α`, `s` is a countable set in `β`, and for all `b` in `s`, `f(b)` is measurable, then the intersection of all `f(b)` for `b` in `s` is a measurable set.
|
MeasurableSpace.generateFrom_le
theorem MeasurableSpace.generateFrom_le :
∀ {α : Type u_1} {s : Set (Set α)} {m : MeasurableSpace α},
(∀ t ∈ s, MeasurableSet t) → MeasurableSpace.generateFrom s ≤ m
The theorem `MeasurableSpace.generateFrom_le` states that for any type `α`, any set `s` of sets of `α`, and any measurable space `m` of `α`, if every set `t` in `s` is a measurable set, then the smallest measure space generated from `s` is less than or equal to `m`. In other words, this theorem ensures that if a set of sets satisfies the property of being measurable, the measure space generated by this set is contained in any other measure space in which the sets are measurable.
More concisely: For any type `α`, any set `s` of measurable subsets of `α`, and any measurable space `m` on `α`, the smallest measurable space generated from `s` is a sub-measure space of `m`.
|
Set.Countable.measurableSet
theorem Set.Countable.measurableSet :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSingletonClass α] {s : Set α},
s.Countable → MeasurableSet s
The theorem `Set.Countable.measurableSet` states that for any type `α` equipped with a measurable space structure and a measurable singleton class, if we have a set `s` of this type which is countable (i.e., there exists an injective map from `s` to the set of natural numbers `ℕ`), then `s` is a measurable set in the ambient measurable space on `α`.
More concisely: If `α` is a type with a measurable space structure and a measurable singleton class, and `s` is a countable (injectively mappeable to `ℕ`) subset of `α`, then `s` is a measurable set in the ambient measurable space on `α`.
|
Mathlib.MeasureTheory.MeasurableSpace.Defs._auxLemma.24
theorem Mathlib.MeasureTheory.MeasurableSpace.Defs._auxLemma.24 :
∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {a : α},
(Measurable fun x => a) = True
This theorem states that for any types `α` and `β`, any measurable spaces `x` over `α` and `x_1` over `β`, and any element `a` of type `α`, the function that maps every element of its domain to the fixed element `a` is measurable. Here, measurability is defined in the sense that the preimage of every measurable set under this function is a measurable set.
More concisely: For any measurable spaces `(α: Type)`, `(β: Type)`, and measurable sets `X: MeasurableSpace α`, `X_1: MeasurableSpace β`, and element `a: α`, the constant function `λ (x: X): β => a` is measurable in the sense that for any measurable set `M ⊆ β`, the preimage `(λ x. a)⁻¹'[M] ⊆ X` is a measurable subset of `X`.
|
MeasurableSet.compl
theorem MeasurableSet.compl :
∀ {α : Type u_1} {s : Set α} {m : MeasurableSpace α}, MeasurableSet s → MeasurableSet sᶜ
The theorem `MeasurableSet.compl` states that for any type `α`, any set `s` of type `α`, and any measurable space `m` on `α`, if the set `s` is measurable in the measurable space `m`, then the complement of `s` (denoted by `sᶜ`) is also measurable in `m`. In mathematical terms, this means that the measurability property is closed under the operation of taking complements in the given measurable space.
More concisely: If `s` is a measurable subset of a measurable space `(α, m)`, then the complement `sᶜ` is also measurable.
|
Mathlib.MeasureTheory.MeasurableSpace.Defs._auxLemma.3
theorem Mathlib.MeasureTheory.MeasurableSpace.Defs._auxLemma.3 :
∀ {α : Type u_1} {m : MeasurableSpace α}, MeasurableSet Set.univ = True
This theorem states that for any given type `α` and any measurable space `m` on `α`, the universal set (i.e., the set of all elements of `α`) is a measurable set. In other words, in the context of measure theory, any possible set of elements drawn from a given type is considered measurable.
More concisely: The universal set of any measurable space is measurable.
|
measurable_discrete
theorem measurable_discrete :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
[inst_2 : DiscreteMeasurableSpace α] (f : α → β), Measurable f
The theorem `measurable_discrete` states that for any two types `α` and `β`, if `α` is equipped with a discrete measurable space structure and `β` with any measurable space structure, then every function `f` from `α` to `β` is measurable. In other words, for any set in `β` that is considered measurable, its preimage under the function `f` is also measurable in `α` when `α` is a discrete measurable space. This holds for every possible function `f` from `α` to `β`.
More concisely: If `α` is a discrete measurable space and `β` is any measurable space, then every function from `α` to `β` is measurable.
|
Mathlib.MeasureTheory.MeasurableSpace.Defs._auxLemma.14
theorem Mathlib.MeasureTheory.MeasurableSpace.Defs._auxLemma.14 :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSingletonClass α] (a : α),
MeasurableSet {a} = True
The theorem `Mathlib.MeasureTheory.MeasurableSpace.Defs._auxLemma.14` states that for any type `α` endowed with a `MeasurableSpace` structure and a `MeasurableSingletonClass` structure, any singleton set, which contains only one element `a` of type `α`, is a measurable set. This is always true regardless of the specific `α`, `MeasurableSpace`, or `MeasurableSingletonClass` in use.
More concisely: For any type `α` equipped with a `MeasurableSpace` and `MeasurableSingletonClass` structure, the singleton set of any element in `α` is measurable.
|
MeasurableSet.insert
theorem MeasurableSet.insert :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSingletonClass α] {s : Set α},
MeasurableSet s → ∀ (a : α), MeasurableSet (insert a s)
The theorem `MeasurableSet.insert` states that for any type `α` equipped with both a `MeasurableSpace` structure and a `MeasurableSingletonClass` structure, if `s` is a set of elements of type `α` that is measurable, then the set resulting from inserting any element `a` of type `α` into `s` is also measurable. This means that measurability is preserved under the operation of inserting an element into a set.
More concisely: If `α` is a type with both `MeasurableSpace` and `MeasurableSingletonClass` structures, and `s` is a measurable subset of `α`, then the subset obtained by inserting an element `a` into `s` is also measurable.
|
MeasurableSpace.generateFrom_sup_generateFrom
theorem MeasurableSpace.generateFrom_sup_generateFrom :
∀ {α : Type u_1} {s t : Set (Set α)},
MeasurableSpace.generateFrom s ⊔ MeasurableSpace.generateFrom t = MeasurableSpace.generateFrom (s ∪ t)
This theorem states that for any type `α` and any two sets of sets `s` and `t` of the type `α`, the supremum of the measure spaces generated from `s` and the measure space generated from `t` is equal to the measure space generated from the union of `s` and `t`. In other words, combining the measure spaces created from two collections of basic sets results in the same measure space as that created from the combined collection of basic sets.
More concisely: Given any type `α` and sets of sets `s` and `t` of type `α`, the measure spaces generated from `s` and `t` have the same supremum as the measure space generated from the union of `s` and `t`.
|
MeasurableSet.of_compl
theorem MeasurableSet.of_compl :
∀ {α : Type u_1} {s : Set α} {m : MeasurableSpace α}, MeasurableSet sᶜ → MeasurableSet s
This theorem states that for any type `α`, any set `s` of type `α`, and any measure space `m` on `α`, if the complement of the set `s` (denoted as `sᶜ`) is a measurable set, then the set `s` itself is also a measurable set. In mathematical terms, if a set's complement is measurable in a given measure space, then the set itself is measurable in that measure space.
More concisely: If a set's complement is measurable in a given measure space, then the set is measurable.
|
MeasurableSet.disjointed
theorem MeasurableSet.disjointed :
∀ {α : Type u_1} {m : MeasurableSpace α} {f : ℕ → Set α},
(∀ (i : ℕ), MeasurableSet (f i)) → ∀ (n : ℕ), MeasurableSet (disjointed f n)
This theorem states that for any type `α` and any measure space `m` on `α`, if we have a sequence `f` of sets of `α` (which can be interpreted as a sequence of measurable events) such that every set in this sequence is a measurable set, then the `n`-th set in the sequence derived from `f` by the `disjointed` function is also a measurable set. In other words, if you take a sequence of measurable sets and subtract each set from the ones following it, resulting in a new sequence of sets where each set is disjoint from the previous ones, each set in this new sequence is also measurable.
More concisely: Given a type `α` and a measure space `m` on `α`, if `f` is a sequence of measurable sets, then the sequence `disjointed f` of pairwise disjoint sets obtained from `f` is also a sequence of measurable sets.
|
MeasurableSet.iInter
theorem MeasurableSet.iInter :
∀ {α : Type u_1} {ι : Sort u_6} {m : MeasurableSpace α} [inst : Countable ι] {f : ι → Set α},
(∀ (b : ι), MeasurableSet (f b)) → MeasurableSet (⋂ b, f b)
The theorem `MeasurableSet.iInter` states that for any type `α`, any type `ι` which is countable, a measurable space `m` on `α`, and a function `f` from `ι` to the sets of `α`, if every set `f b` for each `b` in `ι` is a measurable set, then the intersection of all these sets (represented as `⋂ b, f b`) is also a measurable set. This theorem captures an important property of measurable sets: the countable intersection of measurable sets is also measurable.
More concisely: The countable intersection of measurable sets in a measurable space is measurable.
|
MeasurableSpace.generateFrom_measurableSet
theorem MeasurableSpace.generateFrom_measurableSet :
∀ {α : Type u_1} [inst : MeasurableSpace α], MeasurableSpace.generateFrom {s | MeasurableSet s} = inst
This theorem states that for any type `α` and any instance of a measurable space on `α`, the smallest measure space that contains all the basic sets which are measurable is equivalent to the original instance of the measurable space. In other words, it's asserting that the measurable space generated from the collection of its own measurable sets is the same as the original measurable space itself.
More concisely: The measurable σ-algebra generated by the collection of measurable sets in a measurable space is equal to the original measurable σ-algebra.
|
MeasurableSpace.measurableSet_generateFrom
theorem MeasurableSpace.measurableSet_generateFrom :
∀ {α : Type u_1} {s : Set (Set α)} {t : Set α}, t ∈ s → MeasurableSet t
This theorem states that, for any type `α`, if we have a set `s` where each element is itself a set of `α`, and a set `t` of `α`, then if `t` is an element of `s`, `t` is a measurable set. In other words, any set that is a member of a collection of sets is measurable. This is a fundamental concept of measure theory, where a measurable set is one that we are capable of assigning a "measure" or size to in a coherent manner.
More concisely: If `s` is a set of sets where each element is a set of type `α`, then any element `t` in `s` is a measurable set of type `α`.
|