isPiSystem_Ixx
theorem isPiSystem_Ixx :
∀ {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [inst : LinearOrder α] {Ixx : α → α → Set α} {p : α → α → Prop},
(∀ {a b : α}, (Ixx a b).Nonempty → p a b) →
(∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)) →
∀ (f : ι → α) (g : ι' → α), IsPiSystem {S | ∃ i j, p (f i) (g j) ∧ Ixx (f i) (g j) = S}
The theorem `isPiSystem_Ixx` states that for any type `α` with a linear order, for any two sorts `ι` and `ι'`, for any function `Ixx` from pairs of `α` to sets of `α`, and for any property `p` on pairs of `α`, if `p` holds for any pair `(a, b)` such that the set `Ixx(a, b)` is nonempty, and if the intersection of `Ixx(a₁, b₁)` and `Ixx(a₂, b₂)` is always `Ixx(max(a₁, a₂), min(b₁, b₂))` for any `a₁, b₁, a₂, b₂` in `α`, then for any functions `f` from `ι` to `α` and `g` from `ι'` to `α`, the set of sets `S` such that there exist `i` in `ι` and `j` in `ι'` where `p(f(i), g(j))` holds and `Ixx(f(i), g(j))` equals `S` forms a π-system.
In simpler terms, this theorem states that under certain conditions, a certain set of sets, constructed using the given `Ixx` and property `p`, forms a π-system, which is a family of sets that is closed under finite intersections.
More concisely: Given a type with a linear order, a function from pairs of elements to sets of elements, and a property on pairs, if the property holds for pairs with nonempty sets and intersections follow the given order, then the sets defined by the property and function form a π-system.
|
MeasurableSpace.DynkinSystem.has_iUnion
theorem MeasurableSpace.DynkinSystem.has_iUnion :
∀ {α : Type u_1} (d : MeasurableSpace.DynkinSystem α) {β : Type u_2} [inst : Countable β] {f : β → Set α},
Pairwise (Disjoint on f) → (∀ (i : β), d.Has (f i)) → d.Has (⋃ i, f i)
This theorem states that for any type `α` with a measurable space's dynkin system `d`, and any countable type `β`, if we have a function `f` from `β` to sets of `α` such that the sets `f i` are pairwise disjoint, and each set `f i` is in the dynkin system `d`, then the union of all sets `f i` (over all `i` in `β`) is also in the dynkin system `d`. This essentially says that a dynkin system is closed under countable disjoint unions, provided that each set in the union is also in the dynkin system.
More concisely: If `d` is a measurable space's dynkin system, and `f : β → α` is a function with pairwise disjoint, `d`-measurable sets `fi`, then `⋃i ∈ β fi` is also `d`-measurable.
|
MeasurableSpace.isPiSystem_measurableSet
theorem MeasurableSpace.isPiSystem_measurableSet :
∀ {α : Type u_1} [inst : MeasurableSpace α], IsPiSystem {s | MeasurableSet s}
This theorem states that for any given type `α` that has a measurable space structure, the set of all measurable subsets of `α` forms a π-system. In other words, if `s` and `t` are both measurable subsets of `α` and their intersection is nonempty, then their intersection is also a measurable subset of `α`. This is a property associated with measure theory where a collection of sets that is closed under the operation of intersection is known as a π-system.
More concisely: Given a measurable space `(α, Σ)`, the collection `Σ` of measurable subsets of `α` forms a π-system.
|
IsPiSystem.singleton
theorem IsPiSystem.singleton : ∀ {α : Type u_1} (S : Set α), IsPiSystem {S}
The theorem `IsPiSystem.singleton` states that for any set `S` of any type `α`, the singleton set containing only `S` is a π-system. In other words, any singleton set containing a set `S` is closed under binary intersection, meaning that if two subsets of `S` have a nonempty intersection, then their intersection is also a subset of `S`.
More concisely: For any set `S` of type `α`, the singleton set `{S}` is a π-system, i.e., any two subsets of `S` have nonempty intersection implies their intersection is a subset of `S`.
|
MeasurableSpace.DynkinSystem.generateFrom_eq
theorem MeasurableSpace.DynkinSystem.generateFrom_eq :
∀ {α : Type u_1} {s : Set (Set α)} (hs : IsPiSystem s),
MeasurableSpace.generateFrom s = (MeasurableSpace.DynkinSystem.generate s).toMeasurableSpace ⋯
**Dynkin's π-λ theorem**:
This theorem states that for any given collection of sets that is closed under binary intersections (also known as a π-system), the generated Dynkin system is equivalent to the σ-algebra it generates. This result is popularly referred to as the π-λ theorem. It should be noted that while often a π-system is required to be non-empty, this condition is not enforced in this formalization.
More concisely: A π-system (a collection of sets closed under binary intersections) equals the generated σ-algebra.
|
MeasurableSpace.DynkinSystem.generate_le
theorem MeasurableSpace.DynkinSystem.generate_le :
∀ {α : Type u_1} (d : MeasurableSpace.DynkinSystem α) {s : Set (Set α)},
(∀ t ∈ s, d.Has t) → MeasurableSpace.DynkinSystem.generate s ≤ d
This theorem states that for any type `α`, any Dynkin system `d` on `α`, and any collection `s` of sets of `α`, if every element `t` in `s` is in the Dynkin system `d` (i.e., `d.Has t`), then the Dynkin system generated by `s` is a sub-Dynkin-system of `d`. In other words, any Dynkin system that contains the elements of `s` must also contain the Dynkin system generated by `s`. This represents an essential property of the generated Dynkin system: it's the smallest Dynkin system containing a given collection of sets.
More concisely: If every set in a collection `s` is in a Dynkin system `d`, then the Dynkin system generated by `s` is a sub-Dynkin-system of `d`.
|
MeasurableSpace.DynkinSystem.has_empty
theorem MeasurableSpace.DynkinSystem.has_empty : ∀ {α : Type u_2} (self : MeasurableSpace.DynkinSystem α), self.Has ∅
This theorem states that for any Dynkin system in a measurable space, the empty set is included in the Dynkin system. In other words, given any type `α` and a Dynkin system `self` defined on `α`, the Dynkin system `self` contains the empty set.
More concisely: In any measurable space, the empty set belongs to every Dynkin system.
|
isPiSystem_Ixx_mem
theorem isPiSystem_Ixx_mem :
∀ {α : Type u_1} [inst : LinearOrder α] {Ixx : α → α → Set α} {p : α → α → Prop},
(∀ {a b : α}, (Ixx a b).Nonempty → p a b) →
(∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)) →
∀ (s t : Set α), IsPiSystem {S | ∃ l ∈ s, ∃ u ∈ t, p l u ∧ Ixx l u = S}
This theorem states that for any type `α` with a linear order, given a function `Ixx : α → α → Set α` and a predicate `p : α → α → Prop`, if `p` holds for any `a` and `b` such that `Ixx a b` is nonempty, and if the intersection of `Ixx a₁ b₁` and `Ixx a₂ b₂` equals `Ixx (max a₁ a₂) (min b₁ b₂)` for any `a₁`, `b₁`, `a₂`, `b₂`, then the set of all `S` such that there exist `l` in `s` and `u` in `t` for which `p l u` holds and `Ixx l u` equals `S`, forms a π-system.
In other words, it's a statement about a certain form of structured set, where this set forms a π-system under certain conditions. A π-system is a collection of subsets that is closed under binary intersection of non-disjoint sets. Note that this theorem does not impose any nonempty requirement on the π-system.
More concisely: For any type with a linear order and a binary relation satisfying certain conditions, the collection of sets defined by the relation forms a π-system.
|
isPiSystem_piiUnionInter
theorem isPiSystem_piiUnionInter :
∀ {α : Type u_1} {ι : Type u_2} (π : ι → Set (Set α)),
(∀ (x : ι), IsPiSystem (π x)) → ∀ (S : Set ι), IsPiSystem (piiUnionInter π S)
The theorem `isPiSystem_piiUnionInter` states that for any type `α` and an index type `ι`, if we have a family `π` of π-systems (where a π-system is a collection of subsets of `α` that is closed under binary intersection of non-disjoint sets), then `piiUnionInter π S` is also a π-system for any set `S` of indices `ι`. Here, `piiUnionInter π S` refers to the set of sets that can be expressed as the intersection over elements in some finite subset `t` of `S`, of sets from the corresponding π-systems in `π`. This theorem essentially says that the operation `piiUnionInter` preserves the property of being a π-system when applied to a family of π-systems.
More concisely: Given a type `α` and an index type `ι`, if `π` is a family of π-systems on `α`, then `piiUnionInter π` preserves the property of being a π-system.
|
isPiSystem_image_Iic
theorem isPiSystem_image_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Set α), IsPiSystem (Set.Iic '' s) := by
sorry
This theorem states that for any set `s` of a given type `α` where `α` has a linear order, the image of `s` under the function `Set.Iic`, which denotes the left-infinite right-closed interval, forms a π-system. A π-system is a collection of subsets that is closed under binary intersection of non-disjoint sets. In this case, it means that any two intervals produced by `Set.Iic` from elements of `s` that have a nonempty intersection, also give an interval that is in the image of `s` under `Set.Iic`.
More concisely: Given a set `s` of a linearly ordered type `α`, the image of `s` under `Set.Iic` forms a π-system.
|
isPiSystem_image_Iio
theorem isPiSystem_image_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Set α), IsPiSystem (Set.Iio '' s) := by
sorry
This theorem states that for any set `s` of elements of a certain type `α`, where `α` has a linear order, the image of `s` under the map `Set.Iio` forms a π-system. In other words, if `s` is a set and `Set.Iio` maps each element in `s` to a corresponding left-infinite right-open interval, then the collection of these intervals is a π-system. A π-system is a collection of sets that is closed under binary intersection of non-disjoint sets, meaning that if any two sets in the collection have a non-empty intersection, then their intersection is also in the collection. In this context, the left-infinite right-open intervals generated by `Set.Iio` have this property.
More concisely: For any set `s` of elements from a linearly ordered type `α`, the collection of left-infinite right-open intervals obtained by mapping each element in `s` using `Set.Iio` forms a π-system.
|
MeasurableSpace.DynkinSystem.has_compl
theorem MeasurableSpace.DynkinSystem.has_compl :
∀ {α : Type u_2} (self : MeasurableSpace.DynkinSystem α) {a : Set α}, self.Has a → self.Has aᶜ
This theorem states that a Dynkin system in a measurable space is closed under complementation. Specifically, for any type `α` and any Dynkin system `self` on this type, if a set `a` is an element of this Dynkin system, then its complement `aᶜ` is also an element of the Dynkin system. Here, `Set α` denotes a set of elements of type `α` and `aᶜ` denotes the complement of the set `a`.
More concisely: If `self` is a Dynkin system on type `α`, then for all `a ∈ self`, its complement `aᶜ` also belongs to `self`.
|
MeasurableSpace.DynkinSystem.has_iUnion_nat
theorem MeasurableSpace.DynkinSystem.has_iUnion_nat :
∀ {α : Type u_2} (self : MeasurableSpace.DynkinSystem α) {f : ℕ → Set α},
Pairwise (Disjoint on f) → (∀ (i : ℕ), self.Has (f i)) → self.Has (⋃ i, f i)
The theorem `MeasurableSpace.DynkinSystem.has_iUnion_nat` states that for any Dynkin system on a type `α`, and a sequence `f` of sets of `α` indexed by the natural numbers, if every pair of sets in the sequence `f` are disjoint (their intersection is the empty set), and each set in the sequence `f` belongs to the Dynkin system, then the countable union of the sets in the sequence `f` (i.e., the set of all elements that belong to at least one set in `f`) also belongs to the Dynkin system. In other words, a Dynkin system is closed under the countable union of pairwise disjoint sets. It is suggested to use a more general theorem, `MeasurableSpace.DynkinSystem.has_iUnion`, instead.
More concisely: A Dynkin system is closed under countable unions of pairwise disjoint sets.
|
MeasurableSpace.induction_on_inter
theorem MeasurableSpace.induction_on_inter :
∀ {α : Type u_1} {C : Set α → Prop} {s : Set (Set α)} [m : MeasurableSpace α],
m = MeasurableSpace.generateFrom s →
IsPiSystem s →
C ∅ →
(∀ t ∈ s, C t) →
(∀ (t : Set α), MeasurableSet t → C t → C tᶜ) →
(∀ (f : ℕ → Set α),
Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ i, f i)) →
∀ ⦃t : Set α⦄, MeasurableSet t → C t
This theorem states that, given a type `α`, a property `C` on subsets of `α`, and a set `s` of subsets of `α`, if the measurable space `m` is generated from `s`, `s` is a π-system, `C` holds for the empty set, and `C` holds for each subset in `s`, then the following properties hold:
1. For any subset `t` of `α`, if `t` is measurable and `C` holds for `t`, then `C` holds for the complement of `t`.
2. For any sequence `f` from natural numbers to subsets of `α` such that the images of different natural numbers are pairwise disjoint, if each subset in the sequence is measurable and `C` holds for each subset, then `C` holds for the union of the subsets in the sequence.
Under these conditions, the theorem finally asserts that for any measurable subset `t` of `α`, `C` holds for `t`. This theorem can be seen as an induction principle for proving properties of subsets in a generated measurable space that are closed under complement and countable unions.
More concisely: Given a measurable space generated by a π-system `s` and a property `C` on subsets that holds for the empty set and all subsets in `s`, if `C` preserves complements and countable unions of pairwise disjoint sets, then `C` holds for any measurable subset of the space.
|