Skip to content
This repository has been 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
wants to merge 21 commits into
base: master
Choose a base branch
from
Open

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

wants to merge 21 commits into from

Conversation

eric-wieser
Copy link
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
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot 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
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot 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
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot 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
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot 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
@mathlib-dependent-issues-bot
Copy link
Collaborator

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
@semorrison semorrison 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.
3 participants
@eric-wieser @mathlib-dependent-issues-bot @semorrison