Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[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

    @kex-y
    kex-y 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

    @kex-y
    kex-y 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

    @kex-y
    kex-y 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

    @kex-y
    kex-y 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

    @kex-y
    kex-y 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

    @kex-y
    kex-y 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

    @kex-y
    kex-y 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

    @kex-y
    kex-y 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

    @kex-y
    kex-y 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

    @kex-y
    kex-y 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
    @kex-y
    kex-y 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

    @kex-y
    kex-y 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

    @kex-y
    kex-y 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

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