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

feat(measure_theory/measure/haar_lebesgue): the volume measures on euclidean_space ℝ ι and ι → ℝ agree #19013

Open
eric-wieser wants to merge 21 commits intomasterfrom
eric-wieser/euclidean-measurable-2
Open

feat(measure_theory/measure/haar_lebesgue): the volume measures on euclidean_space ℝ ι and ι → ℝ agree #19013
eric-wieser wants to merge 21 commits intomasterfrom
eric-wieser/euclidean-measurable-2

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser commented May 14, 2023 •
edited by github-actions bot
Loading

@eric-wieser
feat(measure_theory/measure/haar_of_basis): put the canonical measure…
b9e8712 
… on euclidean space
@eric-wieser
add lemma
b59d059
@eric-wieser
wip
006db9c
@eric-wieser
wip
bf341be
@eric-wieser
feat(topology/sets/compacts): add positive_compacts.map
358d353 
Also adds some missing functorial lemmas about `map`
@eric-wieser
chore(measure_theory/measure/haar_of_basis): lemmas about `basis.para…
6ed508e 
…llelepiped`

These are bundled versions of the lemmas about `parallelepiped`.
@eric-wieser
Merge remote-tracking branch 'origin/master' into eric-wieser/trivial…
f8ab07b 
…-basis.parallelepiped-lemmas
@eric-wieser
Merge remote-tracking branch 'origin/master' into eric-wieser/euclide…
f5bb3b5 
…an-measurable-2
@eric-wieser
Merge remote-tracking branch 'origin/eric-wieser/trivial-basis.parall…
0680ec1 
…elepiped-lemmas' into eric-wieser/euclidean-measurable-2
@eric-wieser
fix bad merge
954e92b
@eric-wieser eric-wieser added WIP Work in progress t-measure-probability Measure theory / Probability theory labels May 14, 2023
@eric-wieser eric-wieser requested a review from a team as a code owner May 14, 2023 22:35
@ghost ghost added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label May 14, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label May 15, 2023
@ghost ghost added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label May 16, 2023
@eric-wieser eric-wieser mentioned this pull request May 17, 2023
Closed
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label May 22, 2023
@ghost
Copy link
Copy Markdown

ghost commented May 22, 2023

This PR/issue depends on:

@github-actions github-actions bot added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Jul 15, 2023
@eric-wieser eric-wieser mentioned this pull request Jul 15, 2023
Closed
@kim-em kim-em added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
@eric-wieser eric-wieser mentioned this pull request Sep 5, 2023
Closed
1 task
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

No reviews

Assignees

No one assigned

Labels

modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. t-measure-probability Measure theory / Probability theory too-late This PR was ready too late for inclusion in mathlib3 WIP Work in progress

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@eric-wieser @kim-em