IsOpen.measure_pos
theorem IsOpen.measure_pos :
∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X)
[inst_1 : μ.IsOpenPosMeasure] {U : Set X}, IsOpen U → U.Nonempty → 0 < ↑↑μ U
The theorem `IsOpen.measure_pos` states that for any topological space `X` with a measurable space structure and a measure `μ` that satisfies the property of being an open positive measure, if `U` is an open and nonempty subset of `X`, then the measure of `U` is strictly positive. In other words, it asserts that any nonempty open set in a topological space, when measured with an open positive measure, has a positive measure.
More concisely: If X is a topological space with a measurable structure and μ is an open positive measure, then the measure of any nonempty open subset of X is strictly positive.
|
MeasureTheory.Measure.measure_pos_of_nonempty_interior
theorem MeasureTheory.Measure.measure_pos_of_nonempty_interior :
∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X)
[inst_1 : μ.IsOpenPosMeasure] {s : Set X}, (interior s).Nonempty → 0 < ↑↑μ s
The theorem `MeasureTheory.Measure.measure_pos_of_nonempty_interior` states that for any type `X` with a topological space structure, a measurable space structure, and a measure `μ` that assigns positive values to open sets, if the interior of a set `s` is nonempty, then the measure of the set `s` is positive. In other words, if there exists at least one element in the interior of a set, the measure of the set according to the measure theory is strictly greater than zero.
More concisely: If `X` is a topological space with a measurable structure and `μ` is a measure assigning positive values to open sets, then the measure of a nonempty set `s` with nonempty interior is positive.
|
IsOpen.measure_ne_zero
theorem IsOpen.measure_ne_zero :
∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X)
[inst_1 : μ.IsOpenPosMeasure] {U : Set X}, IsOpen U → U.Nonempty → ↑↑μ U ≠ 0
The theorem `IsOpen.measure_ne_zero` states that for any type `X` with a topological space structure and a measurable space structure, a given measure `μ` of `X` that satisfies the property of being a positive measure on open sets, and any open set `U` of `X`, if `U` is non-empty, then the measure of `U` with respect to `μ` is not equal to zero.
In other words, in the context of measure theory, it asserts that any non-empty open set in a topological space has a non-zero measure under a measure that assigns positive values to open sets.
More concisely: If `X` is a topological space with a measurable structure and `μ` is a positive measure on open sets, then a non-empty open set in `X` has positive measure under `μ`.
|
Metric.measure_ball_pos
theorem Metric.measure_ball_pos :
∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X)
[inst_1 : μ.IsOpenPosMeasure] (x : X) {r : ℝ}, 0 < r → 0 < ↑↑μ (Metric.ball x r)
The theorem `Metric.measure_ball_pos` states that for any given type `X` that has a `PseudoMetricSpace` structure, a measurable space `m`, a measure `μ` on `X` that is open and positive, and any point `x` in `X`, if the radius `r` is greater than zero, then the measure of the ball centered at `x` with radius `r` is also greater than zero. In other words, if we have a positive radius, the measure of the set of all points at a distance less than the radius from a given point is also positive.
More concisely: For any `PseudoMetricSpace` `X` with a `Measure` `μ` that is open and positive, given a point `x` in `X` and a positive radius `r`, the measure of the open ball `Ball x r` is also positive.
|
MeasureTheory.Measure.eq_of_ae_eq
theorem MeasureTheory.Measure.eq_of_ae_eq :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {m : MeasurableSpace X} [inst_1 : TopologicalSpace Y]
[inst_2 : T2Space Y] {μ : MeasureTheory.Measure X} [inst_3 : μ.IsOpenPosMeasure] {f g : X → Y},
μ.ae.EventuallyEq f g → Continuous f → Continuous g → f = g
This theorem states that if two functions `f` and `g`, mapping from a type `X` to a type `Y` (with `X` being a topological space, `Y` being both a topological and T2 space, and `μ` being an open positive measure on `X`), are almost everywhere equal with respect to measure `μ`, and both `f` and `g` are continuous, then `f` and `g` are indeed equal. In mathematical terms, if two continuous functions are equal almost everywhere (except for a set of measure zero), they must be equal everywhere.
More concisely: If `f` and `g` are continuous functions mapping between topological spaces `X` and `Y` (where `X` is a topological space, `Y` is a T2 space, and `μ` is an open positive measure on `X`), and `f` and `g` are almost everywhere equal with respect to `μ`, then `f = g`.
|
MeasureTheory.Measure.eqOn_of_ae_eq
theorem MeasureTheory.Measure.eqOn_of_ae_eq :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {m : MeasurableSpace X} [inst_1 : TopologicalSpace Y]
[inst_2 : T2Space Y] {μ : MeasureTheory.Measure X} [inst_3 : μ.IsOpenPosMeasure] {s : Set X} {f g : X → Y},
(μ.restrict s).ae.EventuallyEq f g →
ContinuousOn f s → ContinuousOn g s → s ⊆ closure (interior s) → Set.EqOn f g s
The theorem, `MeasureTheory.Measure.eqOn_of_ae_eq`, states that for any topological spaces `X` and `Y` with `Y` being a T2 space, any measurable space `X`, any positive open measure `μ` on `X`, and any set `s` of `X`, if two functions `f` and `g` from `X` to `Y` are equal almost everywhere with respect to the measure `μ` restricted to `s`, and both functions are continuous on `s`, and `s` is a subset of the closure of its own interior, then these two functions are equal on `s`. In other words, under these conditions, almost everywhere equality implies equality on the set `s`.
More concisely: If `X` and `Y` are topological spaces with `Y` being T2, `X` is a measurable space with positive open measure `μ`, `s` is a subset of `X` with interior and closure, and functions `f` and `g` from `X` to `Y` are measurable, continuous on `s`, and equal almost everywhere on `s` with respect to `μ`, then `f` and `g` agree on `s`.
|
MeasureTheory.Measure.eqOn_open_of_ae_eq
theorem MeasureTheory.Measure.eqOn_open_of_ae_eq :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {m : MeasurableSpace X} [inst_1 : TopologicalSpace Y]
[inst_2 : T2Space Y] {μ : MeasureTheory.Measure X} [inst_3 : μ.IsOpenPosMeasure] {U : Set X} {f g : X → Y},
(μ.restrict U).ae.EventuallyEq f g → IsOpen U → ContinuousOn f U → ContinuousOn g U → Set.EqOn f g U
This theorem states that for any two functions `f` and `g` mapping from a type `X` to a type `Y`, where `X` is a topological space and `Y` is a T2 (or Hausdorff) space, if these two functions are almost everywhere equal on an open set `U` (according to a measure `μ` restricted to `U`) and both functions are continuous on this set, then the two functions are actually equal on this open set. In other words, if two continuous functions coincide almost everywhere on an open set in a topological space, they actually coincide everywhere on that set as long as the target space is a Hausdorff space.
More concisely: If `f` and `g` are continuous functions from a topological space `X` to a Hausdorff space `Y` such that `μ`-almost every point in an open set `U` has the same image under `f` and `g`, then `f` and `g` agree on all points in `U`.
|
IsOpen.measure_eq_zero_iff
theorem IsOpen.measure_eq_zero_iff :
∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X)
[inst_1 : μ.IsOpenPosMeasure] {U : Set X}, IsOpen U → (↑↑μ U = 0 ↔ U = ∅)
This theorem states that for any type `X` that is equipped with both a topological space structure and a measurable space structure, given a measure `μ` which is a positive measure on open sets, and any set `U` of type `X`, if `U` is an open set (in the topological space sense), then the measure of `U` is zero if and only if `U` is an empty set. In other words, in such a setting, an open set has zero measure precisely when it's the empty set.
More concisely: In the setting of a type `X` with both topological and measurable structures, an open set `U` has measure zero if and only if it is empty.
|
Metric.measure_closedBall_pos
theorem Metric.measure_closedBall_pos :
∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X)
[inst_1 : μ.IsOpenPosMeasure] (x : X) {r : ℝ}, 0 < r → 0 < ↑↑μ (Metric.closedBall x r)
The theorem `Metric.measure_closedBall_pos` states that for any pseudometric space `X`, given a measurable space `X`, a measure `μ` on it which is an open positive measure, and any point `x` in `X`, if `r` is a real number greater than 0, then the measure `μ` of the closed ball centered at `x` with radius `r` is also greater than 0. In other words, the measure of any non-empty closed ball in a pseudometric space with an open positive measure is always positive.
More concisely: In a pseudometric space endowed with an open, positive measure, the measure of any non-empty closed ball is positive.
|
IsNowhereDense.of_isClosed_null
theorem IsNowhereDense.of_isClosed_null :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {s : Set X} {μ : MeasureTheory.Measure X}
[inst_2 : μ.IsOpenPosMeasure], IsClosed s → ↑↑μ s = 0 → IsNowhereDense s
The theorem `IsNowhereDense.of_isClosed_null` states that for any set `s` of type `X`, where `X` is a topological space with measurable space structure and a positive measure `μ`, if `s` is a closed set and the measure of `s` under `μ` is zero, then `s` is a "nowhere dense" set. Here, a set is considered "nowhere dense" if the interior of its closure is an empty set. This theorem essentially shows the link between the measure-theoretic concept of null sets and the topological concept of nowhere dense sets under the condition of closedness. The need for the set being closed is highlighted with the example of rational numbers, which although countable and hence of measure zero, are dense and not nowhere dense.
More concisely: A closed set with measure zero in a topological space with a measurable structure is nowhere dense.
|
IsOpen.eq_empty_of_measure_zero
theorem IsOpen.eq_empty_of_measure_zero :
∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X}
[inst_1 : μ.IsOpenPosMeasure] {U : Set X}, IsOpen U → ↑↑μ U = 0 → U = ∅
The theorem `IsOpen.eq_empty_of_measure_zero` states that given any type `X` with a topology and a measurable space structure, and a measure `μ` on `X` that is an "open positive measure", if `U` is an open set in `X` such that the measure of `U` is zero, then `U` must be the empty set. In other words, an open set in a space equipped with an open positive measure, which has zero measure, is necessarily empty.
More concisely: An open set in a measurable space equipped with an open positive measure having zero measure is empty.
|
MeasureTheory.Measure.interior_eq_empty_of_null
theorem MeasureTheory.Measure.interior_eq_empty_of_null :
∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X}
[inst_1 : μ.IsOpenPosMeasure] {s : Set X}, ↑↑μ s = 0 → interior s = ∅
This theorem states that for any set `s` in a given type `X` which is equipped with a topology and a measurable space, and given a measure `μ` on `X` which is a positive measure on open sets, if the measure of the set `s` is zero (i.e., `s` is a null set), then the interior of `s` is empty. In other words, a null set in a measure space with a positive measure on open sets does not contain any open subsets, hence its interior is empty.
More concisely: A null set in a measure space with a positive measure on open sets has an empty interior.
|
IsMeagre.of_isSigmaCompact_null
theorem IsMeagre.of_isSigmaCompact_null :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {s : Set X} {μ : MeasureTheory.Measure X}
[inst_2 : μ.IsOpenPosMeasure] [inst_3 : T2Space X], IsSigmaCompact s → ↑↑μ s = 0 → IsMeagre s
This theorem states that a σ-compact measure zero subset is meagre, or in other words, thin or negligible, in the context of a topological space. More generally, any Fσ set (a countable union of closed sets) with measure zero is also meagre. The theorem requires a few conditions: the space needs both topological and measurable structures, the measure on the space must have positive values on nonempty open sets, and the space must be a T2 space (a space where any two distinct points have disjoint open neighborhoods). If these conditions are satisfied, and given that a set is σ-compact and has a measure of zero, then the set is meagre.
More concisely: In a T2 topological space endowed with a measure having positive values on nonempty open sets, any σ-compact set with measure zero is meagre.
|