Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-18 05:49 bb1b56c7

View on Github →

feat(algebra/indicator_function): smul lemmas for functions (#12059) And a few basic lemmas in set/basic.

Estimated changes

Modified src/algebra/indicator_function.lean

added theorem set.indicator_const_smul

added theorem set.indicator_const_smul_apply

modified theorem set.indicator_smul

modified theorem set.indicator_smul_apply

Modified src/analysis/box_integral/integrability.lean

Modified src/data/finsupp/basic.lean

Modified src/data/set/basic.lean

added theorem set.compl_range_inl

added theorem set.compl_range_inr

Modified src/logic/nonempty.lean

added theorem function.surjective.nonempty