Theorems · Theorem · measure theory

MeasureTheory.tendsto_measure_compl_closedBall_of_isTightMeasureSet

∀ {E : Type u_1} {mE : MeasurableSpace E} {S : Set (MeasureTheory.Measure E)} [inst : PseudoMetricSpace E],
  MeasureTheory.IsTightMeasureSet S →
    ∀ (x : E), Filter.Tendsto (fun r => ⨆ μ ∈ S, μ (Metric.closedBall x r)ᶜ) Filter.atTop (nhds 0)

Defined in: Mathlib.MeasureTheory.Measure.TightNormed
Cited by: 2 results in Mathlib
Foundations: Depth 171 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: PseudoMetricSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites24

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
Realstatement and proof · cited by 25,697
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ENNRealstatement and proof · cited by 9,879
Filterproof · cited by 8,121
nhdsstatement and proof · cited by 5,554
Filter.Tendstostatement and proof · cited by 3,814
Compl.complstatement and proof · cited by 2,925
iSupstatement and proof · cited by 2,415
Filter.atTopstatement and proof · cited by 2,405

Cited by2

Results whose statement or proof uses this declaration.

MeasureTheory.tendsto_measure_norm_gt_of_isTightMeasureSetproof · cited by 2
MeasureTheory.isTightMeasureSet_iff_tendsto_measure_compl_closedBallproof · cited by 0