Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-28 17:35 7236938c

View on Github →

feat(measure_theory/measure_space): add count_apply_infinite (#3592) Also add some supporting lemmas about set.infinite.

Estimated changes

Modified src/data/fintype/basic.lean

added theorem infinite.exists_subset_card_eq

Modified src/data/set/finite.lean

added theorem set.infinite.exists_subset_card_eq

added theorem set.infinite.to_subtype

added theorem set.infinite_coe_iff

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.measure.count_apply_eq_top

added theorem measure_theory.measure.count_apply_finite

added theorem measure_theory.measure.count_apply_infinite

added theorem measure_theory.measure.count_apply_lt_top