Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-02 13:45 4fe734da

View on Github →

fix(algebra/indicator_function): add missing decidable instances to lemma statements (#13834) This keeps the definition of set.indicator as non-computable, but ensures that when lemmas are applied they generalize to any decidable instances.

Estimated changes

Modified src/algebra/indicator_function.lean

modified theorem set.comp_mul_indicator

deleted def set.indicator

deleted def set.mul_indicator

modified theorem set.mul_indicator_apply

deleted def set.mul_indicator_hom

modified theorem set.piecewise_eq_mul_indicator

Modified src/combinatorics/simple_graph/inc_matrix.lean

deleted def simple_graph.inc_matrix

Modified src/geometry/euclidean/circumcenter.lean

Modified src/measure_theory/function/conditional_expectation.lean

Modified src/measure_theory/function/uniform_integrable.lean

Modified src/measure_theory/integral/bochner.lean

modified theorem measure_theory.simple_func.integral_eq_sum_filter

modified theorem measure_theory.simple_func.integral_eq_sum_of_subset

Modified src/measure_theory/probability_mass_function/monad.lean

Modified src/topology/instances/ennreal.lean