Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-21 10:07 d8cde2aa

View on Github →

feat(measure_theory/interval_integral): more versions of FTC-1 (#3709) Left/right derivative, strict derivative, differentiability in both endpoints. Other changes:

  • rename filter.tendsto_le_left and filter.tendsto_le_right to filter.tendsto.mono_left and filter.tendsto.mono_right, swap arguments;
  • rename order_top.tendsto_at_top to order_top.tendsto_at_top_nhds;
  • introduce tendsto_Ixx_class instead of is_interval_generated.

Estimated changes

modified theorem filter.tendsto_infi'
deleted theorem filter.tendsto_le_left
deleted theorem filter.tendsto_le_right
modified theorem filter.tendsto.Icc
modified theorem filter.tendsto.Ico
modified theorem filter.tendsto.Ioc
modified theorem filter.tendsto.Ioo
deleted theorem filter.tendsto.Ixx
deleted theorem order_top.tendsto_at_top