Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-28 03:23 4b5bf56b

View on Github →

feat(measure_theory/integral/interval_integral): one more FTC-2 (#9409)

Estimated changes

Modified src/measure_theory/integral/interval_integral.lean

modified theorem interval_integral.integral_eq_integral_of_support_subset

added theorem interval_integral.integral_eq_sub_of_has_deriv_at_of_tendsto

Modified src/topology/continuous_on.lean

added theorem continuous_within_at_update_same

added theorem filter.eventually_eq.congr_continuous_within_at

Modified src/topology/separation.lean

added theorem continuous_on_update_iff

added theorem continuous_within_at_update_of_ne

added theorem ne.nhds_within_compl_singleton