# Documentation

Mathlib.MeasureTheory.Lattice

# 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

class MeasurableSup (M : Type u_1) [] [Sup M] :

We say that a type has MeasurableSup if (c ⊔ ·) and (· ⊔ c) are measurable functions. For a typeclass assuming measurability of uncurry (· ⊔ ·) see MeasurableSup₂.

Instances
class MeasurableSup₂ (M : Type u_1) [] [Sup M] :

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
class MeasurableInf (M : Type u_1) [] [Inf M] :

We say that a type has MeasurableInf if (c ⊓ ·) and (· ⊓ c) are measurable functions. For a typeclass assuming measurability of uncurry (· ⊓ ·) see MeasurableInf₂.

Instances
class MeasurableInf₂ (M : Type u_1) [] [Inf M] :

We say that a type has MeasurableInf₂ if uncurry (· ⊓ ·) is a measurable functions. For a typeclass assuming measurability of (c ⊓ ·) and (· ⊓ c) see MeasurableInf.

Instances
instance OrderDual.instMeasurableSup {M : Type u_1} [] [Inf M] [] :
instance OrderDual.instMeasurableInf {M : Type u_1} [] [Sup M] [] :
instance OrderDual.instMeasurableSup₂ {M : Type u_1} [] [Inf M] [] :
instance OrderDual.instMeasurableInf₂ {M : Type u_1} [] [Sup M] [] :
theorem Measurable.const_sup {M : Type u_1} [] {α : Type u_2} {m : } {f : αM} [Sup M] [] (hf : ) (c : M) :
Measurable fun x => c f x
theorem AEMeasurable.const_sup {M : Type u_1} [] {α : Type u_2} {m : } {μ : } {f : αM} [Sup M] [] (hf : ) (c : M) :
AEMeasurable fun x => c f x
theorem Measurable.sup_const {M : Type u_1} [] {α : Type u_2} {m : } {f : αM} [Sup M] [] (hf : ) (c : M) :
Measurable fun x => f x c
theorem AEMeasurable.sup_const {M : Type u_1} [] {α : Type u_2} {m : } {μ : } {f : αM} [Sup M] [] (hf : ) (c : M) :
AEMeasurable fun x => f x c
theorem Measurable.sup' {M : Type u_1} [] {α : Type u_2} {m : } {f : αM} {g : αM} [Sup M] [] (hf : ) (hg : ) :
theorem Measurable.sup {M : Type u_1} [] {α : Type u_2} {m : } {f : αM} {g : αM} [Sup M] [] (hf : ) (hg : ) :
Measurable fun a => f a g a
theorem AEMeasurable.sup' {M : Type u_1} [] {α : Type u_2} {m : } {μ : } {f : αM} {g : αM} [Sup M] [] (hf : ) (hg : ) :
theorem AEMeasurable.sup {M : Type u_1} [] {α : Type u_2} {m : } {μ : } {f : αM} {g : αM} [Sup M] [] (hf : ) (hg : ) :
AEMeasurable fun a => f a g a
instance MeasurableSup₂.toMeasurableSup {M : Type u_1} [] [Sup M] [] :
theorem Measurable.const_inf {M : Type u_1} [] {α : Type u_2} {m : } {f : αM} [Inf M] [] (hf : ) (c : M) :
Measurable fun x => c f x
theorem AEMeasurable.const_inf {M : Type u_1} [] {α : Type u_2} {m : } {μ : } {f : αM} [Inf M] [] (hf : ) (c : M) :
AEMeasurable fun x => c f x
theorem Measurable.inf_const {M : Type u_1} [] {α : Type u_2} {m : } {f : αM} [Inf M] [] (hf : ) (c : M) :
Measurable fun x => f x c
theorem AEMeasurable.inf_const {M : Type u_1} [] {α : Type u_2} {m : } {μ : } {f : αM} [Inf M] [] (hf : ) (c : M) :
AEMeasurable fun x => f x c
theorem Measurable.inf' {M : Type u_1} [] {α : Type u_2} {m : } {f : αM} {g : αM} [Inf M] [] (hf : ) (hg : ) :
theorem Measurable.inf {M : Type u_1} [] {α : Type u_2} {m : } {f : αM} {g : αM} [Inf M] [] (hf : ) (hg : ) :
Measurable fun a => f a g a
theorem AEMeasurable.inf' {M : Type u_1} [] {α : Type u_2} {m : } {μ : } {f : αM} {g : αM} [Inf M] [] (hf : ) (hg : ) :
theorem AEMeasurable.inf {M : Type u_1} [] {α : Type u_2} {m : } {μ : } {f : αM} {g : αM} [Inf M] [] (hf : ) (hg : ) :
AEMeasurable fun a => f a g a
instance MeasurableInf₂.to_hasMeasurableInf {M : Type u_1} [] [Inf M] [] :
theorem Finset.measurable_sup' {α : Type u_2} {m : } {δ : Type u_3} [] [] [] {ι : Type u_4} {s : } (hs : ) {f : ιδα} (hf : ∀ (n : ι), n sMeasurable (f n)) :
theorem Finset.measurable_range_sup' {α : Type u_2} {m : } {δ : Type u_3} [] [] [] {f : δα} {n : } (hf : ∀ (k : ), k nMeasurable (f k)) :
theorem Finset.measurable_range_sup'' {α : Type u_2} {m : } {δ : Type u_3} [] [] [] {f : δα} {n : } (hf : ∀ (k : ), k nMeasurable (f k)) :
Measurable fun x => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) fun k => f k x