Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-06 07:07 d3b1d65d

View on Github →

lint(measure_theory): docstrings and style (#4455)

Estimated changes

Modified src/measure_theory/category/Meas.lean

Modified src/measure_theory/measurable_space.lean

Modified src/measure_theory/probability_mass_function.lean

modified def pmf.bernoulli

modified theorem pmf.bind_apply

modified def pmf.of_fintype

modified def pmf.pure

modified def pmf.seq

modified theorem pmf.tsum_coe

modified def {u}