# Borel (measurable) space #

## Main definitions #

`borel α`

: the least`σ`

-algebra that contains all open sets;`class borel_space`

: a space with`topological_space`

and`measurable_space`

structures such that`‹measurable_space α› = borel α`

;`class opens_measurable_space`

: a space with`topological_space`

and`measurable_space`

structures such that all open sets are measurable; equivalently,`borel α ≤ ‹measurable_space α›`

.`borel_space`

instances on`empty`

,`unit`

,`bool`

,`nat`

,`int`

,`rat`

;`measurable`

and`borel_space`

instances on`ℝ`

,`ℝ≥0`

,`ℝ≥0∞`

.

## Main statements #

`is_open.measurable_set`

,`is_closed.measurable_set`

: open and closed sets are measurable;`continuous.measurable`

: a continuous function is measurable;`continuous.measurable2`

: if`f : α → β`

and`g : α → γ`

are measurable and`op : β × γ → δ`

is continuous, then`λ x, op (f x, g y)`

is measurable;`measurable.add`

etc : dot notation for arithmetic operations on`measurable`

predicates, and similarly for`dist`

and`edist`

;`ae_measurable.add`

: similar dot notation for almost everywhere measurable functions;`measurable.ennreal*`

: special cases for arithmetic operations on`ℝ≥0∞`

.

`measurable_space`

structure generated by `topological_space`

.

## Equations

- borel α = measurable_space.generate_from {s : set α | is_open s}

A space with `measurable_space`

and `topological_space`

structures such that
all open sets are measurable.

A space with `measurable_space`

and `topological_space`

structures such that
the `σ`

-algebra of measurable sets is exactly the `σ`

-algebra generated by open sets.

## Instances

In a `borel_space`

all open sets are measurable.

If `s`

is a measurable set, then `𝓝[s] a`

is a measurably generated filter for
each `a`

. This cannot be an `instance`

because it depends on a non-instance `hs : measurable_set s`

.

A continuous function from an `opens_measurable_space`

to a `borel_space`

is measurable.

A continuous function from an `opens_measurable_space`

to a `borel_space`

is ae-measurable.

A homeomorphism between two Borel spaces is a measurable equivalence.

## Equations

- h.to_measurable_equiv = {to_equiv := h.to_equiv, measurable_to_fun := _, measurable_inv_fun := _}

**Alias** of `measurable_of_monotone`

.

`liminf`

over a general filter is measurable. See `measurable_liminf`

for the version over `ℕ`

.

`limsup`

over a general filter is measurable. See `measurable_limsup`

for the version over `ℕ`

.

`liminf`

over `ℕ`

is measurable. See `measurable_liminf'`

for a version with a general filter.

`limsup`

over `ℕ`

is measurable. See `measurable_limsup'`

for a version with a general filter.

Convert a `homeomorph`

to a `measurable_equiv`

.

## Equations

- homemorph.to_measurable_equiv h = {to_equiv := h.to_equiv, measurable_to_fun := _, measurable_inv_fun := _}

## Equations

## Equations

## Equations

## Equations

## Equations

The intervals `(-(n + 1), (n + 1))`

form a finite spanning sets in the set of open intervals
with rational endpoints for a locally finite measure `μ`

on `ℝ`

.

The set of finite `ℝ≥0∞`

numbers is `measurable_equiv`

to `ℝ≥0`

.

`ℝ≥0∞`

is `measurable_equiv`

to `ℝ≥0 ⊕ unit`

.

## Equations

- ennreal.ennreal_equiv_sum = {to_equiv := {to_fun := (equiv.option_equiv_sum_punit ℝ≥0).to_fun, inv_fun := (equiv.option_equiv_sum_punit ℝ≥0).inv_fun, left_inv := ennreal.ennreal_equiv_sum._proof_1, right_inv := ennreal.ennreal_equiv_sum._proof_2}, measurable_to_fun := ennreal.ennreal_equiv_sum._proof_3, measurable_inv_fun := ennreal.ennreal_equiv_sum._proof_4}

note: `ℝ≥0∞`

can probably be generalized in a future version of this lemma.

The set of finite `ereal`

numbers is `measurable_equiv`

to `ℝ`

.

A limit (over a general filter) of measurable `ℝ≥0`

valued functions is measurable.
The assumption `hs`

can be dropped using `filter.is_countably_generated.has_antimono_basis`

, but we
don't need that case yet.

A sequential limit of measurable `ℝ≥0`

valued functions is measurable.

A limit (over a general filter) of measurable functions valued in a metric space is measurable.
The assumption `hs`

can be dropped using `filter.is_countably_generated.has_antimono_basis`

, but we
don't need that case yet.

A sequential limit of measurable functions valued in a metric space is measurable.