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.

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

feat: port MeasureTheory.Constructions.Prod.Basic #4168

Closed
wants to merge 105 commits into from

Commits on May 16, 2023

  1. Configuration menu
    Copy the full SHA
    0b718b0 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    9d3c729 View commit details
    Browse the repository at this point in the history
  3. automated fixes

    Mathbin -> Mathlib
    fix certain import statements
    move "by" to end of line
    add import to Mathlib.lean
    Komyyy committed May 16, 2023
    Configuration menu
    Copy the full SHA
    997cdc6 View commit details
    Browse the repository at this point in the history
  4. fix

    Komyyy committed May 16, 2023
    Configuration menu
    Copy the full SHA
    c862990 View commit details
    Browse the repository at this point in the history
  5. fix

    Komyyy committed May 16, 2023
    Configuration menu
    Copy the full SHA
    ce2555b View commit details
    Browse the repository at this point in the history
  6. Fix imports

    urkud committed May 16, 2023
    Configuration menu
    Copy the full SHA
    077a467 View commit details
    Browse the repository at this point in the history
  7. Fix more

    urkud committed May 16, 2023
    Configuration menu
    Copy the full SHA
    09be11b View commit details
    Browse the repository at this point in the history
  8. Fix more

    urkud committed May 16, 2023
    Configuration menu
    Copy the full SHA
    9f825b6 View commit details
    Browse the repository at this point in the history
  9. borelize

    Komyyy committed May 16, 2023
    Configuration menu
    Copy the full SHA
    fe8ffb0 View commit details
    Browse the repository at this point in the history
  10. borelize

    Komyyy committed May 16, 2023
    Configuration menu
    Copy the full SHA
    9d88ac7 View commit details
    Browse the repository at this point in the history
  11. Configuration menu
    Copy the full SHA
    b501d57 View commit details
    Browse the repository at this point in the history
  12. fix

    Komyyy committed May 16, 2023
    Configuration menu
    Copy the full SHA
    7e488be View commit details
    Browse the repository at this point in the history
  13. fix

    Komyyy committed May 16, 2023
    Configuration menu
    Copy the full SHA
    5403d20 View commit details
    Browse the repository at this point in the history
  14. Merge branch 'Filter.iInf_isMeasurablyGenerated' into port/MeasureThe…

    …ory.Constructions.BorelSpace.Basic
    Komyyy committed May 16, 2023
    Configuration menu
    Copy the full SHA
    1701692 View commit details
    Browse the repository at this point in the history
  15. fix

    Komyyy committed May 16, 2023
    Configuration menu
    Copy the full SHA
    4d0942c View commit details
    Browse the repository at this point in the history
  16. fix

    Komyyy committed May 16, 2023
    Configuration menu
    Copy the full SHA
    d0617a2 View commit details
    Browse the repository at this point in the history

Commits on May 17, 2023

  1. borelize

    Komyyy committed May 17, 2023
    Configuration menu
    Copy the full SHA
    c579ecc View commit details
    Browse the repository at this point in the history
  2. fix

    Komyyy committed May 17, 2023
    Configuration menu
    Copy the full SHA
    d8d4166 View commit details
    Browse the repository at this point in the history
  3. fix

    Komyyy committed May 17, 2023
    Configuration menu
    Copy the full SHA
    b9f174c View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    ed7779c View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    4e5490c View commit details
    Browse the repository at this point in the history
  6. automated fixes

    Mathbin -> Mathlib
    fix certain import statements
    move "by" to end of line
    add import to Mathlib.lean
    Komyyy committed May 17, 2023
    Configuration menu
    Copy the full SHA
    938c1ec View commit details
    Browse the repository at this point in the history
  7. Merge branch 'port/MeasureTheory.Constructions.BorelSpace.Basic' into…

    … port/MeasureTheory.Function.SimpleFunc
    Komyyy committed May 17, 2023
    Configuration menu
    Copy the full SHA
    51ac57a View commit details
    Browse the repository at this point in the history
  8. fix

    Komyyy committed May 17, 2023
    Configuration menu
    Copy the full SHA
    aef6c9e View commit details
    Browse the repository at this point in the history
  9. fix

    Komyyy committed May 17, 2023
    Configuration menu
    Copy the full SHA
    3c000d0 View commit details
    Browse the repository at this point in the history
  10. fix

    Komyyy committed May 17, 2023
    Configuration menu
    Copy the full SHA
    07f611a View commit details
    Browse the repository at this point in the history
  11. Configuration menu
    Copy the full SHA
    b5a8222 View commit details
    Browse the repository at this point in the history
  12. Configuration menu
    Copy the full SHA
    18e3037 View commit details
    Browse the repository at this point in the history
  13. automated fixes

    Mathbin -> Mathlib
    fix certain import statements
    move "by" to end of line
    add import to Mathlib.lean
    Komyyy committed May 17, 2023
    Configuration menu
    Copy the full SHA
    464a1de View commit details
    Browse the repository at this point in the history
  14. Merge branch 'port/MeasureTheory.Function.SimpleFunc' into port/Measu…

    …reTheory.Integral.Lebesgue
    Komyyy committed May 17, 2023
    Configuration menu
    Copy the full SHA
    ade1261 View commit details
    Browse the repository at this point in the history
  15. fix

    Komyyy committed May 17, 2023
    Configuration menu
    Copy the full SHA
    b9cb833 View commit details
    Browse the repository at this point in the history

Commits on May 18, 2023

  1. Configuration menu
    Copy the full SHA
    9ba769f View commit details
    Browse the repository at this point in the history
  2. fix

    Komyyy committed May 18, 2023
    Configuration menu
    Copy the full SHA
    bb1d8ed View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    af0848a View commit details
    Browse the repository at this point in the history
  4. preserve argument order

    ChrisHughes24 committed May 18, 2023
    Configuration menu
    Copy the full SHA
    1ca1917 View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    d21e25d View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    a50e3f3 View commit details
    Browse the repository at this point in the history
  7. Merge remote-tracking branch 'origin/SortUnionLift' into Filter.iInf_…

    …isMeasurablyGenerated
    Komyyy committed May 18, 2023
    Configuration menu
    Copy the full SHA
    50f1431 View commit details
    Browse the repository at this point in the history
  8. universe uι

    Komyyy committed May 18, 2023
    Configuration menu
    Copy the full SHA
    d770199 View commit details
    Browse the repository at this point in the history
  9. Merge branch 'Filter.iInf_isMeasurablyGenerated' into port/MeasureThe…

    …ory.Constructions.BorelSpace.Basic
    Komyyy committed May 18, 2023
    Configuration menu
    Copy the full SHA
    909d546 View commit details
    Browse the repository at this point in the history
  10. Merge branch 'port/MeasureTheory.Constructions.BorelSpace.Basic' into…

    … port/MeasureTheory.Function.SimpleFunc
    Komyyy committed May 18, 2023
    Configuration menu
    Copy the full SHA
    d88eaf6 View commit details
    Browse the repository at this point in the history
  11. Merge branch 'port/MeasureTheory.Function.SimpleFunc' into port/Measu…

    …reTheory.Integral.Lebesgue
    Komyyy committed May 18, 2023
    Configuration menu
    Copy the full SHA
    f776bb4 View commit details
    Browse the repository at this point in the history

Commits on May 19, 2023

  1. forward-port

    Komyyy committed May 19, 2023
    Configuration menu
    Copy the full SHA
    9ced134 View commit details
    Browse the repository at this point in the history
  2. Merge branch 'port/MeasureTheory.Constructions.BorelSpace.Basic' into…

    … port/MeasureTheory.Function.SimpleFunc
    Komyyy committed May 19, 2023
    Configuration menu
    Copy the full SHA
    96aae1f View commit details
    Browse the repository at this point in the history
  3. Merge branch 'port/MeasureTheory.Function.SimpleFunc' into port/Measu…

    …reTheory.Integral.Lebesgue
    Komyyy committed May 19, 2023
    Configuration menu
    Copy the full SHA
    b44e633 View commit details
    Browse the repository at this point in the history
  4. style

    Komyyy committed May 19, 2023
    Configuration menu
    Copy the full SHA
    0807592 View commit details
    Browse the repository at this point in the history
  5. Merge branch 'MeasureTheory.Measure.FiniteSpanningSetsIn.set' into po…

    …rt/MeasureTheory.Constructions.BorelSpace.Basic
    Komyyy committed May 19, 2023
    Configuration menu
    Copy the full SHA
    4d1ff4d View commit details
    Browse the repository at this point in the history
  6. Merge branch 'port/MeasureTheory.Constructions.BorelSpace.Basic' into…

    … port/MeasureTheory.Function.SimpleFunc
    Komyyy committed May 19, 2023
    Configuration menu
    Copy the full SHA
    2a2fb79 View commit details
    Browse the repository at this point in the history
  7. Merge branch 'port/MeasureTheory.Function.SimpleFunc' into port/Measu…

    …reTheory.Integral.Lebesgue
    Komyyy committed May 19, 2023
    Configuration menu
    Copy the full SHA
    a293b0e View commit details
    Browse the repository at this point in the history
  8. style

    Komyyy committed May 19, 2023
    Configuration menu
    Copy the full SHA
    5a54f06 View commit details
    Browse the repository at this point in the history
  9. Merge branch 'port/MeasureTheory.Constructions.BorelSpace.Basic' into…

    … port/MeasureTheory.Function.SimpleFunc
    Komyyy committed May 19, 2023
    Configuration menu
    Copy the full SHA
    5a2fb03 View commit details
    Browse the repository at this point in the history
  10. Merge branch 'port/MeasureTheory.Function.SimpleFunc' into port/Measu…

    …reTheory.Integral.Lebesgue
    Komyyy committed May 19, 2023
    Configuration menu
    Copy the full SHA
    9c76e03 View commit details
    Browse the repository at this point in the history
  11. Configuration menu
    Copy the full SHA
    f0c3b27 View commit details
    Browse the repository at this point in the history
  12. Configuration menu
    Copy the full SHA
    6526f8a View commit details
    Browse the repository at this point in the history
  13. automated fixes

    Mathbin -> Mathlib
    fix certain import statements
    move "by" to end of line
    add import to Mathlib.lean
    Komyyy committed May 19, 2023
    Configuration menu
    Copy the full SHA
    d47a6ef View commit details
    Browse the repository at this point in the history
  14. Merge branch 'port/MeasureTheory.Integral.Lebesgue' into port/Measure…

    …Theory.Measure.GiryMonad
    Komyyy committed May 19, 2023
    Configuration menu
    Copy the full SHA
    29ff20b View commit details
    Browse the repository at this point in the history
  15. fix

    Komyyy committed May 19, 2023
    Configuration menu
    Copy the full SHA
    bbc5e82 View commit details
    Browse the repository at this point in the history
  16. Configuration menu
    Copy the full SHA
    be66147 View commit details
    Browse the repository at this point in the history

Commits on May 20, 2023

  1. Configuration menu
    Copy the full SHA
    993834a View commit details
    Browse the repository at this point in the history
  2. namespace

    Komyyy committed May 20, 2023
    Configuration menu
    Copy the full SHA
    045b44a View commit details
    Browse the repository at this point in the history
  3. Merge branch 'port/MeasureTheory.Constructions.BorelSpace.Basic' into…

    … port/MeasureTheory.Function.SimpleFunc
    Komyyy committed May 20, 2023
    Configuration menu
    Copy the full SHA
    48a6db3 View commit details
    Browse the repository at this point in the history
  4. Merge branch 'port/MeasureTheory.Function.SimpleFunc' into port/Measu…

    …reTheory.Integral.Lebesgue
    Komyyy committed May 20, 2023
    Configuration menu
    Copy the full SHA
    91c0e69 View commit details
    Browse the repository at this point in the history
  5. Merge branch 'port/MeasureTheory.Integral.Lebesgue' into port/Measure…

    …Theory.Measure.GiryMonad
    Komyyy committed May 20, 2023
    Configuration menu
    Copy the full SHA
    9e131f3 View commit details
    Browse the repository at this point in the history

Commits on May 21, 2023

  1. Configuration menu
    Copy the full SHA
    a37b5d1 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    4de2362 View commit details
    Browse the repository at this point in the history
  3. automated fixes

    Mathbin -> Mathlib
    fix certain import statements
    move "by" to end of line
    add import to Mathlib.lean
    Komyyy committed May 21, 2023
    Configuration menu
    Copy the full SHA
    93568e5 View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    3854938 View commit details
    Browse the repository at this point in the history
  5. Merge branch 'port/MeasureTheory.Measure.GiryMonad' into port/Measure…

    …Theory.Constructions.Prod.Basic
    Komyyy committed May 21, 2023
    Configuration menu
    Copy the full SHA
    11c0ca6 View commit details
    Browse the repository at this point in the history
  6. fix

    Komyyy committed May 21, 2023
    Configuration menu
    Copy the full SHA
    6010e59 View commit details
    Browse the repository at this point in the history
  7. refactor

    Komyyy committed May 21, 2023
    Configuration menu
    Copy the full SHA
    97c1e90 View commit details
    Browse the repository at this point in the history
  8. lint

    Komyyy committed May 21, 2023
    Configuration menu
    Copy the full SHA
    9d1f9dd View commit details
    Browse the repository at this point in the history
  9. Configuration menu
    Copy the full SHA
    6dac35f View commit details
    Browse the repository at this point in the history
  10. Configuration menu
    Copy the full SHA
    996437d View commit details
    Browse the repository at this point in the history
  11. fix

    Komyyy committed May 21, 2023
    Configuration menu
    Copy the full SHA
    7d7c9a9 View commit details
    Browse the repository at this point in the history
  12. fix

    Komyyy committed May 21, 2023
    Configuration menu
    Copy the full SHA
    375e152 View commit details
    Browse the repository at this point in the history

Commits on May 22, 2023

  1. Configuration menu
    Copy the full SHA
    2afa49c View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    4812fba View commit details
    Browse the repository at this point in the history
  3. SProd

    Komyyy committed May 22, 2023
    Configuration menu
    Copy the full SHA
    24c28f8 View commit details
    Browse the repository at this point in the history
  4. remove note

    Komyyy committed May 22, 2023
    Configuration menu
    Copy the full SHA
    5e57a8c View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    729eb79 View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    182ec1c View commit details
    Browse the repository at this point in the history
  7. correct porting note

    Komyyy committed May 22, 2023
    Configuration menu
    Copy the full SHA
    f7c60ee View commit details
    Browse the repository at this point in the history
  8. Configuration menu
    Copy the full SHA
    e54245b View commit details
    Browse the repository at this point in the history

Commits on May 24, 2023

  1. Configuration menu
    Copy the full SHA
    4ca4be3 View commit details
    Browse the repository at this point in the history
  2. fix

    Komyyy committed May 24, 2023
    Configuration menu
    Copy the full SHA
    10fc6c8 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    ac6094a View commit details
    Browse the repository at this point in the history
  4. 'B' comes before 'a' in unicode

    kmill committed May 24, 2023
    Configuration menu
    Copy the full SHA
    aa71c90 View commit details
    Browse the repository at this point in the history
  5. organize tests

    kmill committed May 24, 2023
    Configuration menu
    Copy the full SHA
    0f0523c View commit details
    Browse the repository at this point in the history
  6. comment out set_option

    kmill committed May 24, 2023
    Configuration menu
    Copy the full SHA
    1762ed9 View commit details
    Browse the repository at this point in the history
  7. Configuration menu
    Copy the full SHA
    99b3d95 View commit details
    Browse the repository at this point in the history
  8. Configuration menu
    Copy the full SHA
    c313628 View commit details
    Browse the repository at this point in the history

Commits on May 25, 2023

  1. Configuration menu
    Copy the full SHA
    cec8772 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    ac36c87 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    9878c19 View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    7fc8d1f View commit details
    Browse the repository at this point in the history
  5. test

    Komyyy committed May 25, 2023
    Configuration menu
    Copy the full SHA
    b860e4d View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    529e0ab View commit details
    Browse the repository at this point in the history
  7. Configuration menu
    Copy the full SHA
    a4b9552 View commit details
    Browse the repository at this point in the history

Commits on May 26, 2023

  1. Configuration menu
    Copy the full SHA
    30c6d64 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    3d36dd3 View commit details
    Browse the repository at this point in the history
  3. Filter.prod

    Komyyy committed May 26, 2023
    Configuration menu
    Copy the full SHA
    a472adc View commit details
    Browse the repository at this point in the history
  4. fix

    Komyyy committed May 26, 2023
    Configuration menu
    Copy the full SHA
    8f34b35 View commit details
    Browse the repository at this point in the history
  5. fix

    Komyyy committed May 26, 2023
    Configuration menu
    Copy the full SHA
    8f928c3 View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    7213954 View commit details
    Browse the repository at this point in the history
  7. forward port

    Komyyy committed May 26, 2023
    Configuration menu
    Copy the full SHA
    f5695a2 View commit details
    Browse the repository at this point in the history