54 General topology

TheoremLebesgue's decomposition theorem#

The Lebesgue decomposition theorem: Any s-finite measure μ has Lebesgue decomposition with respect to any σ-finite measure ν. That is to say, there exist a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.withDensity f

MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite.{u_1} {α : Type u_1}
  {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SFinite μ]
  [MeasureTheory.SigmaFinite ν] : μ.HaveLebesgueDecomposition ν
Sources
MathlibMeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite
Uses 9 · Used by 3
Statement usesAssociative algebra over a commutative ring · Carathéodory's theorem (measure theory) · Integral of positive measurable functions · Linear map · Measurable function
Proof usesCharacteristic p · Characteristic zero · Monotone convergence theorem (1000+ theorems) · Squeeze theorem
Used byLebesgue differentiation theorem · Lebesgue's density theorem · Differentiability of integrals with respect to parameters

TheoremLebesgue's density theorem#

Given an arbitrary set s, then μ (s ∩ closedBall x r) / μ (closedBall x r) converges to 1 when r tends to 0, for almost every x in s. This shows that almost every point of s is a Lebesgue density point for s. A stronger version holds for measurable sets, see ae_tendsto_measure_inter_div_of_measurableSet.

See also IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div.

Besicovitch.ae_tendsto_measure_inter_div.{u} {β : Type u} [MetricSpace β] [MeasurableSpace β]
  [BorelSpace β] [SecondCountableTopology β] [HasBesicovitchCovering β]
  (μ : MeasureTheory.Measure β) [MeasureTheory.IsLocallyFiniteMeasure μ] (s : Set β) :
  ∀ᵐ (x : β) ∂μ.restrict s,
    Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r))
      (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)
Sources
MathlibBesicovitch.ae_tendsto_measure_inter_div
Uses 8 · Used by 1
Statement usesAlmost sure convergence · Associative algebra over a commutative ring · Borel sigma-algebra · Carathéodory's theorem (measure theory) · Linear map · Metric space · Positive measure
Proof usesLebesgue's decomposition theorem
Used byChange of variables formula

TheoremMetrization theorems#

Urysohn's metrization theorem (Tychonoff's version): a T₃ topological space with second countable topology X is metrizable, i.e., there exists a metric space structure that generates the same topology.

TopologicalSpace.metrizableSpace_of_t3_secondCountable.{u_1} (X : Type u_1) [TopologicalSpace X]
  [T3Space X] [SecondCountableTopology X] : TopologicalSpace.MetrizableSpace X

Urysohn's metrization theorem (only).

Sources
MathlibTopologicalSpace.metrizableSpace_of_t3_secondCountable
Uses 6
Statement usesNatural number · Uniform space
Proof usesInduced topology · Infinite sum · Topology of a metric space · Urysohn's lemma

TheoremTietze extension theorem#

Tietze extension theorem for real-valued bounded continuous maps, a version with a closed embedding and unbundled composition. If e : C(X, Y) is a closed embedding of a topological space into a normal topological space and f : X →ᵇ ℝ is a bounded continuous function, then there exists a bounded continuous function g : Y →ᵇ ℝ of the same norm such that g ∘ e = f.

BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y]
  (f : BoundedContinuousFunction X ℝ) {e : X → Y} (he : Topology.IsClosedEmbedding e) :
  ∃ g, ‖g‖ = ‖f‖ ∧ ⇑g ∘ e = ⇑f
Sources
MathlibBoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding
Uses 9
Statement usesContinuous function · Induced topology · Metric space
Proof usesClosed map · Completeness of R · Completeness of spaces of bounded continuous functions · Lipschitz continuity · List · Urysohn's lemma

TheoremTychonoff's theorem#

Tychonoff's theorem: product of compact sets is compact.

isCompact_pi_infinite.{u_1, u_2} {ι : Type u_1} {X : ι → Type u_2}
  [(i : ι) → TopologicalSpace (X i)] {s : (i : ι) → Set (X i)} :
  (∀ (i : ι), IsCompact (s i)) → IsCompact {x | ∀ (i : ι), x i ∈ s i}
Sources
MathlibisCompact_pi_infinite
Uses 2 · Used by 1
Statement usesCompactness in terms of filters
Proof usesLimit of a map with respect to filters
Used byBanach–Alaoglu theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.