Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(measure_theory/interval_integral): FTC-2 #4945

Closed
wants to merge 24 commits into from
Closed

[Merged by Bors] - feat(measure_theory/interval_integral): FTC-2 #4945

wants to merge 24 commits into from

Commits on Nov 8, 2020

  1. ftc-2

    @benjamindavidson
    benjamindavidson committed Nov 8, 2020
    Configuration menu
    Copy the full SHA
    b20be0a View commit details
    Browse the repository at this point in the history

Commits on Nov 9, 2020

  1. ftc-2

    @benjamindavidson
    benjamindavidson committed Nov 9, 2020
    Configuration menu
    Copy the full SHA
    26c22fe View commit details
    Browse the repository at this point in the history

  2. chore(data/finset/basic): use has_coe_t for coercion of finset to… 

    … `set` (#4917)
    @urkud @benjamindavidson
    urkud authored and benjamindavidson committed Nov 9, 2020
    Configuration menu
    Copy the full SHA
    5dfee89 View commit details
    Browse the repository at this point in the history

  3. feat(data/set/intervals/basic): collection of lemmas of the form I??_… 

    …of_I?? (#4918)

Some propositions about intervals that I thought may be useful (despite their simplicity).
    @benjamindavidson
    benjamindavidson committed Nov 9, 2020
    Configuration menu
    Copy the full SHA
    f81be76 View commit details
    Browse the repository at this point in the history

  4. chore(data/finset/basic): trivial simp lemmas (#4950)

    @urkud @benjamindavidson
    urkud authored and benjamindavidson committed Nov 9, 2020
    Configuration menu
    Copy the full SHA
    81b3324 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'ftc2' of https://github.com/leanprover-community/mathlib … 

    …into ftc2
    @benjamindavidson
    benjamindavidson committed Nov 9, 2020
    Configuration menu
    Copy the full SHA
    e43624f View commit details
    Browse the repository at this point in the history

  6. Merge branch 'master' of https://github.com/leanprover-community/mathlib 

     into ftc2

update
    @benjamindavidson
    benjamindavidson committed Nov 9, 2020
    Configuration menu
    Copy the full SHA
    e7ea8b4 View commit details
    Browse the repository at this point in the history

  7. lint (test)

    @benjamindavidson
    benjamindavidson committed Nov 9, 2020
    Configuration menu
    Copy the full SHA
    b52285e View commit details
    Browse the repository at this point in the history

Commits on Nov 11, 2020

  1. ftc-2

    @benjamindavidson
    benjamindavidson committed Nov 11, 2020
    Configuration menu
    Copy the full SHA
    f9d3bb6 View commit details
    Browse the repository at this point in the history

  2. lint (test)

    @benjamindavidson
    benjamindavidson committed Nov 11, 2020
    Configuration menu
    Copy the full SHA
    201a55e View commit details
    Browse the repository at this point in the history

  3. Merge branch 'ftc2' of https://github.com/leanprover-community/mathlib … 

    …into ftc2
    @benjamindavidson
    benjamindavidson committed Nov 11, 2020
    Configuration menu
    Copy the full SHA
    bff5fc9 View commit details
    Browse the repository at this point in the history

Commits on Nov 22, 2020

  1. Merge branch 'master' into ftc2

    @urkud
    urkud committed Nov 22, 2020
    Configuration menu
    Copy the full SHA
    74bf6d1 View commit details
    Browse the repository at this point in the history

  2. Fix some statements (not proofs)

    @urkud
    urkud committed Nov 22, 2020
    Configuration menu
    Copy the full SHA
    85418fc View commit details
    Browse the repository at this point in the history

Commits on Dec 9, 2020

  1. Fixed eq_of_right_deriv_eq, eq_of_deriv_eq

    @benjamindavidson
    benjamindavidson committed Dec 9, 2020
    Configuration menu
    Copy the full SHA
    b4beb3f View commit details
    Browse the repository at this point in the history

Commits on Dec 14, 2020

  1. completed has_deriv_within_at_right_integrable

    @benjamindavidson
    benjamindavidson committed Dec 14, 2020
    Configuration menu
    Copy the full SHA
    3dfa1d2 View commit details
    Browse the repository at this point in the history

Commits on Dec 19, 2020

  1. Merge branch 'master' into ftc2

    @urkud
    urkud committed Dec 19, 2020
    Configuration menu
    Copy the full SHA
    f960c75 View commit details
    Browse the repository at this point in the history

  2. Drop an unused lemma

    @urkud
    urkud committed Dec 19, 2020
    Configuration menu
    Copy the full SHA
    71147d1 View commit details
    Browse the repository at this point in the history

  3. Fix, golf, move

    @urkud
    urkud committed Dec 19, 2020
    Configuration menu
    Copy the full SHA
    03cc5d2 View commit details
    Browse the repository at this point in the history

  4. Fix

    @urkud
    urkud committed Dec 19, 2020
    Configuration menu
    Copy the full SHA
    81b0706 View commit details
    Browse the repository at this point in the history

Commits on Dec 22, 2020

  1. Merge branch 'master' into ftc2

    @urkud
    urkud committed Dec 22, 2020
    Configuration menu
    Copy the full SHA
    ad49e91 View commit details
    Browse the repository at this point in the history

  2. Fix

    @urkud
    urkud committed Dec 22, 2020
    Configuration menu
    Copy the full SHA
    b0e822b View commit details
    Browse the repository at this point in the history

Commits on Dec 25, 2020

  1. docstrings

    @benjamindavidson
    benjamindavidson committed Dec 25, 2020
    Configuration menu
    Copy the full SHA
    687fe77 View commit details
    Browse the repository at this point in the history

Commits on Dec 26, 2020

  1. Merge branch 'master' into ftc2

    @urkud
    urkud committed Dec 26, 2020
    Configuration menu
    Copy the full SHA
    6df448d View commit details
    Browse the repository at this point in the history

  2. Merge branch 'ftc2' of git://github.com/leanprover-community/mathlib … 

    …into ftc2
    @urkud
    urkud committed Dec 26, 2020
    Configuration menu
    Copy the full SHA
    14e3474 View commit details
    Browse the repository at this point in the history