# Typeclasses for measurability of lattice operations #

In this file we define classes `MeasurableSup`

and `MeasurableInf`

and prove dot-style
lemmas (`Measurable.sup`

, `AEMeasurable.sup`

etc). For binary operations we define two typeclasses:

`MeasurableSup`

says that both left and right sup are measurable;`MeasurableSup₂`

says that`fun p : α × α => p.1 ⊔ p.2`

is measurable,

and similarly for other binary operations. The reason for introducing these classes is that in case
of topological space `α`

equipped with the Borel `σ`

-algebra, instances for `MeasurableSup₂`

etc require `α`

to have a second countable topology.

For instances relating, e.g., `ContinuousSup`

to `MeasurableSup`

see file
`MeasureTheory.BorelSpace`

.

## Tags #

measurable function, lattice operation

- measurable_const_sup : ∀ (c : M), Measurable fun x => c ⊔ x
- measurable_sup_const : ∀ (c : M), Measurable fun x => x ⊔ c

We say that a type has `MeasurableSup`

if `(c ⊔ ·)`

and `(· ⊔ c)`

are measurable functions.
For a typeclass assuming measurability of `uncurry (· ⊔ ·)`

see `MeasurableSup₂`

.

## Instances

- measurable_sup : Measurable fun p => p.fst ⊔ p.snd

We say that a type has `MeasurableSup₂`

if `uncurry (· ⊔ ·)`

is a measurable functions.
For a typeclass assuming measurability of `(c ⊔ ·)`

and `(· ⊔ c)`

see `MeasurableSup`

.

## Instances

- measurable_const_inf : ∀ (c : M), Measurable fun x => c ⊓ x
- measurable_inf_const : ∀ (c : M), Measurable fun x => x ⊓ c

We say that a type has `MeasurableInf`

if `(c ⊓ ·)`

and `(· ⊓ c)`

are measurable functions.
For a typeclass assuming measurability of `uncurry (· ⊓ ·)`

see `MeasurableInf₂`

.

## Instances

- measurable_inf : Measurable fun p => p.fst ⊓ p.snd

We say that a type has `MeasurableInf₂`

if `uncurry (· ⊓ ·)`

is a measurable functions.
For a typeclass assuming measurability of `(c ⊓ ·)`

and `(· ⊓ c)`

see `MeasurableInf`

.