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: tendsto_of_integral_tendsto_of_monotone #11167

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat: tendsto_of_integral_tendsto_of_monotone #11167

wants to merge 8 commits into from

Commits on Mar 5, 2024

  1. feat: tendsto_of_integral_tendsto_of_monotone

    @RemyDegenne
    RemyDegenne committed Mar 5, 2024
    Configuration menu
    Copy the full SHA
    ec7594c View commit details
    Browse the repository at this point in the history

Commits on Mar 6, 2024

  1. add tendsto_of_lintegral_tendsto_of_antitone

    @RemyDegenne
    RemyDegenne committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    bc16399 View commit details
    Browse the repository at this point in the history

  2. deprecate; suffices from; golf using dual

    @RemyDegenne
    RemyDegenne committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    2251dd6 View commit details
    Browse the repository at this point in the history

  3. docstrings

    @RemyDegenne
    RemyDegenne committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    56dac68 View commit details
    Browse the repository at this point in the history

Commits on Mar 8, 2024

  1. remove aemeasurable assumption

    @sgouezel
    sgouezel committed Mar 8, 2024
    Configuration menu
    Copy the full SHA
    b9bfb4b View commit details
    Browse the repository at this point in the history

  2. appease linter

    @sgouezel
    sgouezel committed Mar 8, 2024
    Configuration menu
    Copy the full SHA
    b6fa446 View commit details
    Browse the repository at this point in the history

  3. fix build

    @sgouezel
    sgouezel committed Mar 8, 2024
    Configuration menu
    Copy the full SHA
    9fcec6c View commit details
    Browse the repository at this point in the history

Commits on Mar 9, 2024

  1. add deprecated dates

    @RemyDegenne
    RemyDegenne committed Mar 9, 2024
    Configuration menu
    Copy the full SHA
    7eef760 View commit details
    Browse the repository at this point in the history