finite_measure_weak_convergence): Change to probability theory notations. (#17231)

Commit

3 years ago

chore(measure_theory/measure/finite_measure_weak_convergence): Change to probability theory notations. (#17231) Change notations of the underlying measurable spaces from α to Ω.

Author

kkytola

Parents

7a7d4dd4

mathlib 8315f58e - chore(measure_theory/measure/finite_measure_weak_convergence): Change to probability theory notations. (#17231)

mathlib
8315f58e - chore(measure_theory/measure/finite_measure_weak_convergence): Change to probability theory notations. (#17231)