Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-06 00:02 8f424fca

View on Github →

chore(measure_theory/pi): a few more lemmas (#5604) Also prove that a locally finite measure in a second_countable_topology is sigma_finite.

Estimated changes

Modified src/algebra/big_operators/order.lean

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.measure.exists_is_open_measure_lt_top

added theorem measure_theory.measure.finite_at_filter.exists_mem_basis

added theorem measure_theory.measure.sigma_finite_of_countable

added theorem measure_theory.measure.sigma_finite_of_not_nonempty

Modified src/measure_theory/pi.lean

added theorem measure_theory.measure.pi_eval_preimage_null

added theorem measure_theory.measure.pi_hyperplane

added theorem measure_theory.measure_space.pi_def

added theorem measure_theory.volume_pi