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/order/upper_lower): Order-connected sets in ℝⁿ are measurable #16976

Closed
wants to merge 51 commits into from
Closed

[Merged by Bors] - feat(measure_theory/order/upper_lower): Order-connected sets in ℝⁿ are measurable #16976

wants to merge 51 commits into from

Commits on Jul 20, 2022

  1. initial commit

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

  2. is_upper_set.exists_subset_ball

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

  3. initial commit

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

Commits on Jul 21, 2022

  1. done

    @YaelDillies
    YaelDillies committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    4df4f1f View commit details
    Browse the repository at this point in the history

  2. whoops #lint

    @YaelDillies
    YaelDillies committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    79c4912 View commit details
    Browse the repository at this point in the history

  3. fix lemma names

    @YaelDillies
    YaelDillies committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    266e92f View commit details
    Browse the repository at this point in the history

  4. upper_closure_inter_lower_closure

    @YaelDillies
    YaelDillies committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    41b5386 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin/upper_closure' into ord_connecte… 

    …d_measurable
    @YaelDillies
    YaelDillies committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    ecea181 View commit details
    Browse the repository at this point in the history

  6. bump upper_lower

    @YaelDillies
    YaelDillies committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    12ba02c View commit details
    Browse the repository at this point in the history

Commits on Aug 8, 2022

  1. Merge remote-tracking branch 'origin/master' into ord_connected_measu… 

    …rable
    @YaelDillies
    YaelDillies committed Aug 8, 2022
    Configuration menu
    Copy the full SHA
    4810e00 View commit details
    Browse the repository at this point in the history

  2. stupid api

    @YaelDillies
    YaelDillies committed Aug 8, 2022
    Configuration menu
    Copy the full SHA
    b317f46 View commit details
    Browse the repository at this point in the history

Commits on Sep 29, 2022

  1. Merge remote-tracking branch 'origin/master' into ord_connected_measu… 

    …rable
    @YaelDillies
    YaelDillies committed Sep 29, 2022
    Configuration menu
    Copy the full SHA
    edab706 View commit details
    Browse the repository at this point in the history

Commits on Sep 30, 2022

  1. most of the glue

    @YaelDillies
    YaelDillies committed Sep 30, 2022
    Configuration menu
    Copy the full SHA
    c9ba9c8 View commit details
    Browse the repository at this point in the history

Commits on Oct 2, 2022

  1. fix false statement

    @YaelDillies
    YaelDillies committed Oct 2, 2022
    Configuration menu
    Copy the full SHA
    cfdffbb View commit details
    Browse the repository at this point in the history

Commits on Oct 13, 2022

  1. Merge remote-tracking branch 'origin/master' into ord_connected_measu… 

    …rable
    @YaelDillies
    YaelDillies committed Oct 13, 2022
    Configuration menu
    Copy the full SHA
    ef6bd56 View commit details
    Browse the repository at this point in the history

  2. done 🎉

    @YaelDillies
    YaelDillies committed Oct 13, 2022
    Configuration menu
    Copy the full SHA
    883e764 View commit details
    Browse the repository at this point in the history

Commits on Oct 14, 2022

  1. feat(topology/algebra/order/upper_lower): The closure of an upper set

    @YaelDillies
    YaelDillies committed Oct 14, 2022
    Configuration menu
    Copy the full SHA
    30042d4 View commit details
    Browse the repository at this point in the history

  2. module docs

    @YaelDillies
    YaelDillies committed Oct 14, 2022
    Configuration menu
    Copy the full SHA
    8a6f06f View commit details
    Browse the repository at this point in the history

  3. map of upper sets 

    upper sets form a monoid
upper set of open is open
antichains have measure zero
    @YaelDillies
    YaelDillies committed Oct 14, 2022
    Configuration menu
    Copy the full SHA
    c37628d View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into ord_connected_measu… 

    …rable
    @YaelDillies
    YaelDillies committed Oct 14, 2022
    Configuration menu
    Copy the full SHA
    88fc03c View commit details
    Browse the repository at this point in the history

Commits on Oct 15, 2022

  1. bump 

    more map API
    @YaelDillies
    YaelDillies committed Oct 15, 2022
    Configuration menu
    Copy the full SHA
    9707a7c View commit details
    Browse the repository at this point in the history

Commits on Oct 23, 2022

  1. Merge remote-tracking branch 'origin/master' into ord_connected_measu… 

    …rable
    @YaelDillies
    YaelDillies committed Oct 23, 2022
    Configuration menu
    Copy the full SHA
    db47c8a View commit details
    Browse the repository at this point in the history

  2. bump

    @YaelDillies
    YaelDillies committed Oct 23, 2022
    Configuration menu
    Copy the full SHA
    5f96813 View commit details
    Browse the repository at this point in the history

Commits on Oct 29, 2022

  1. Merge remote-tracking branch 'origin/master' into upper_lower_topology

    @YaelDillies
    YaelDillies committed Oct 29, 2022
    Configuration menu
    Copy the full SHA
    d6f0b6b View commit details
    Browse the repository at this point in the history

  2. thickening lemmas

    @YaelDillies
    YaelDillies committed Oct 29, 2022
    Configuration menu
    Copy the full SHA
    c46c8c4 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/master' into ord_connected_measu… 

    …rable
    @YaelDillies
    YaelDillies committed Oct 29, 2022
    Configuration menu
    Copy the full SHA
    cc1d5b5 View commit details
    Browse the repository at this point in the history

  4. bump

    @YaelDillies
    YaelDillies committed Oct 29, 2022
    Configuration menu
    Copy the full SHA
    caf6bc4 View commit details
    Browse the repository at this point in the history

Commits on Oct 30, 2022

  1. remove norm results

    @YaelDillies
    YaelDillies committed Oct 30, 2022
    Configuration menu
    Copy the full SHA
    ee5ab57 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into upper_lower_topology

    @YaelDillies
    YaelDillies committed Oct 30, 2022
    Configuration menu
    Copy the full SHA
    8dd0cbb View commit details
    Browse the repository at this point in the history

  3. revert analysis.normed.order.basic

    @YaelDillies
    YaelDillies committed Oct 30, 2022
    Configuration menu
    Copy the full SHA
    9f6dd28 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into ord_connected_measu… 

    …rable
    @YaelDillies
    YaelDillies committed Oct 30, 2022
    Configuration menu
    Copy the full SHA
    732c1a5 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin/upper_lower_topology' into ord_c… 

    …onnected_measurable
    @YaelDillies
    YaelDillies committed Oct 30, 2022
    Configuration menu
    Copy the full SHA
    0ef8440 View commit details
    Browse the repository at this point in the history

  6. split topological and norm results

    @YaelDillies
    YaelDillies committed Oct 30, 2022
    Configuration menu
    Copy the full SHA
    1c8cb08 View commit details
    Browse the repository at this point in the history

Commits on Oct 31, 2022

  1. Merge remote-tracking branch 'origin/master' into ord_connected_measu… 

    …rable
    @YaelDillies
    YaelDillies committed Oct 31, 2022
    Configuration menu
    Copy the full SHA
    cf68d2b View commit details
    Browse the repository at this point in the history

Commits on Nov 3, 2022

  1. Merge remote-tracking branch 'origin/master' into ord_connected_measu… 

    …rable
    @YaelDillies
    YaelDillies committed Nov 3, 2022
    Configuration menu
    Copy the full SHA
    3c9cd84 View commit details
    Browse the repository at this point in the history

  2. bump

    @YaelDillies
    YaelDillies committed Nov 3, 2022
    Configuration menu
    Copy the full SHA
    884cfc7 View commit details
    Browse the repository at this point in the history

  3. bdd_below.closure

    @YaelDillies
    YaelDillies committed Nov 3, 2022
    Configuration menu
    Copy the full SHA
    09e8aec View commit details
    Browse the repository at this point in the history

Commits on Nov 16, 2022

  1. Merge remote-tracking branch 'origin/master' into ord_connected_measu… 

    …rable
    @YaelDillies
    YaelDillies committed Nov 16, 2022
    Configuration menu
    Copy the full SHA
    d19297d View commit details
    Browse the repository at this point in the history

  2. bump

    @YaelDillies
    YaelDillies committed Nov 16, 2022
    Configuration menu
    Copy the full SHA
    56576cd View commit details
    Browse the repository at this point in the history

Commits on Mar 15, 2023

  1. Merge remote-tracking branch 'origin/master' into ord_connected_measu… 

    …rable
    @YaelDillies
    YaelDillies committed Mar 15, 2023
    Configuration menu
    Copy the full SHA
    199c1f0 View commit details
    Browse the repository at this point in the history

Commits on Mar 21, 2023

  1. boundedness of neighborhoods

    @YaelDillies
    YaelDillies committed Mar 21, 2023
    Configuration menu
    Copy the full SHA
    23683c3 View commit details
    Browse the repository at this point in the history

  2. dedup lemmas

    @YaelDillies
    YaelDillies committed Mar 21, 2023
    Configuration menu
    Copy the full SHA
    2f00905 View commit details
    Browse the repository at this point in the history

  3. generalise data.set.finite lemmas

    @YaelDillies
    YaelDillies committed Mar 21, 2023
    Configuration menu
    Copy the full SHA
    fe46aa8 View commit details
    Browse the repository at this point in the history

Commits on Mar 22, 2023

  1. fix data.set.finite

    @YaelDillies
    YaelDillies committed Mar 22, 2023
    Configuration menu
    Copy the full SHA
    dccaa55 View commit details
    Browse the repository at this point in the history

Commits on Mar 23, 2023

  1. unsorry

    @YaelDillies
    YaelDillies committed Mar 23, 2023
    Configuration menu
    Copy the full SHA
    1d8de6a View commit details
    Browse the repository at this point in the history

  2. fix measure_theory.order.upper_lower

    @YaelDillies
    YaelDillies committed Mar 23, 2023
    Configuration menu
    Copy the full SHA
    e0ff2a8 View commit details
    Browse the repository at this point in the history

Commits on Mar 24, 2023

  1. Merge remote-tracking branch 'origin/master' into ord_connected_measu… 

    …rable
    @YaelDillies
    YaelDillies committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    8ed9a64 View commit details
    Browse the repository at this point in the history

  2. bump

    @YaelDillies
    YaelDillies committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    591ab22 View commit details
    Browse the repository at this point in the history

Commits on Sep 19, 2023

  1. Merge remote-tracking branch 'origin/master' into ord_connected_measu… 

    …rable
    @YaelDillies
    YaelDillies committed Sep 19, 2023
    Configuration menu
    Copy the full SHA
    0665e3c View commit details
    Browse the repository at this point in the history

  2. move lemmas

    @YaelDillies
    YaelDillies committed Sep 19, 2023
    Configuration menu
    Copy the full SHA
    74370c4 View commit details
    Browse the repository at this point in the history

Commits on Oct 16, 2023

  1. forward pointer

    @YaelDillies
    YaelDillies committed Oct 16, 2023
    Configuration menu
    Copy the full SHA
    0d69e7c View commit details
    Browse the repository at this point in the history