mathlib3
refactor(measure_theory/borel): `borel` is not an `instance`
#2326

Merged

refactor(measure_theory/borel): `borel` is not an `instance` #2326

mergify merged 11 commits into master from borel-space

Define `borel_space`

a0c2a1ca

Snapshot

466b57cc

urkud added needs-documentation

urkud added awaiting-review

Drop some unused args, thanks linter

173bc707

Add a module docstring

a318d6d3

Drop a duplicate argument

c881019b

urkud removed needs-documentation

sgouezel commented on 2020-04-06

robertylewis removed awaiting-review

robertylewis added awaiting-author

Apply suggestions from code review

e8fa17f4

Get `ennreal_equiv_nnreal` from a `homeomorph`

efbef615

Merge branch 'borel-space' of git://github.com/leanprover-community/m…

7954586f

Done.

2fd36bd5

urkud removed awaiting-author

urkud added awaiting-review

Fix compile

ba3865e6

sgouezel approved these changes on 2020-04-07

sgouezel removed awaiting-review

sgouezel added ready-to-merge

Merge branch 'master' into borel-space

5c43ddcc

mergify merged 6f75c57e into master 5 years ago

mergify deleted the borel-space branch 5 years ago

Reviewers

sgouezel

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone