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/constructions/borel_space): the set of points for which a measurable sequence of functions converges is measurable #15307

Closed
wants to merge 15 commits into from
Closed

[Merged by Bors] - feat(measure_theory/constructions/borel_space): the set of points for which a measurable sequence of functions converges is measurable #15307

wants to merge 15 commits into from

Commits on Jul 13, 2022

  1. initial commit

    @JasonKYi
    JasonKYi committed Jul 13, 2022
    Configuration menu
    Copy the full SHA
    ee521d1 View commit details
    Browse the repository at this point in the history

  2. add @[measurability] and doc string

    @JasonKYi
    JasonKYi committed Jul 13, 2022
    Configuration menu
    Copy the full SHA
    ac4438c View commit details
    Browse the repository at this point in the history

  3. fix

    @RemyDegenne
    RemyDegenne committed Jul 13, 2022
    Configuration menu
    Copy the full SHA
    435c990 View commit details
    Browse the repository at this point in the history

  4. generalize to polish spaces

    @JasonKYi
    JasonKYi committed Jul 13, 2022
    Configuration menu
    Copy the full SHA
    313e752 View commit details
    Browse the repository at this point in the history

  5. use letI instead of haveI

    @JasonKYi
    JasonKYi committed Jul 13, 2022
    Configuration menu
    Copy the full SHA
    ed790f3 View commit details
    Browse the repository at this point in the history

Commits on Jul 20, 2022

  1. add has_antitone_basis.map

    @JasonKYi
    JasonKYi committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    2b71021 View commit details
    Browse the repository at this point in the history

  2. need cache

    @JasonKYi
    JasonKYi committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    64eab78 View commit details
    Browse the repository at this point in the history

  3. hopefully fix

    @JasonKYi
    JasonKYi committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    5401aa2 View commit details
    Browse the repository at this point in the history

  4. remove unused lemma

    @JasonKYi
    JasonKYi committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    d2ae664 View commit details
    Browse the repository at this point in the history

  5. fix name

    @JasonKYi
    JasonKYi committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    7b53f69 View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2022

  1. remove condition

    @JasonKYi
    JasonKYi committed Jul 24, 2022
    Configuration menu
    Copy the full SHA
    bd8f5db View commit details
    Browse the repository at this point in the history

Commits on Jul 26, 2022

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

     into JasonKYi/set_converges_meas
    @JasonKYi
    JasonKYi committed Jul 26, 2022
    Configuration menu
    Copy the full SHA
    e4eb417 View commit details
    Browse the repository at this point in the history

  2. change name

    @JasonKYi
    JasonKYi committed Jul 26, 2022
    Configuration menu
    Copy the full SHA
    d7e1977 View commit details
    Browse the repository at this point in the history

  3. maybe fix

    @JasonKYi
    JasonKYi committed Jul 26, 2022
    Configuration menu
    Copy the full SHA
    b29e925 View commit details
    Browse the repository at this point in the history

  4. fix

    @JasonKYi
    JasonKYi committed Jul 26, 2022
    Configuration menu
    Copy the full SHA
    7d41340 View commit details
    Browse the repository at this point in the history