Theorem ProbabilityTheory.IsLocalizingSequence.isPrelocalizingSequence_inf_extraction

Modification history

2026-04-04 13:13
Mathlib/Probability/Process/LocalProperty.lean
feat(Probability): Local and stable properties (#33375) …
Added ProbabilityTheory.IsLocalizingSequence.isPrelocalizingSequence_inf_extractionView on Github →