Skip to content

Commit

Permalink
chore(measure_theory/measure/finite_measure_weak_convergence): Split …
Browse files Browse the repository at this point in the history 
…one file to three. (#17332)

Split the file `measure_theory/measure/finite_measure_weak_convergence.lean` into three files in the same folder: `finite_measure.lean`, `probability_measure.lean`, and `portmanteau.lean`.
  • Loading branch information
@kkytola
kkytola committed Nov 5, 2022
1 parent 03fda91 commit 96e43cc
Show file tree
Hide file tree
Showing 4 changed files with 1,513 additions and 1,404 deletions.

0 comments on commit 96e43cc

Please sign in to comment.